Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: No-free-lunch theorem for mach...

Email Gateway (Sep 01 2025 at 20:28):

From: Tobias Nipkow <nipkow@in.tum.de>
No-free-lunch theorem for machine learning
Michikazu Hirata

This entry is a formalization of the no-free-lunch theorem for machine learning
following Section 5.1 of the book Understanding Machine Learning: From Theory to
Algorithms by Shai Shalev-Shwartz and Shai Ben-David. The theorem states that
for binary classification prediction tasks, there is no universal learner,
meaning that for every learning algorithms, there exists a distribution on which
it fails.

https://www.isa-afp.org/entries/No_Free_Lunch_ML.html

Enjoy!

smime.p7s

Last updated: Sep 13 2025 at 04:22 UTC