Get our free extension to see links to code for papers anywhere online!

Chrome logo Add to Chrome

Firefox logo Add to Firefox

A Formal Proof of PAC Learnability for Decision Stumps

Nov 01, 2019
Joseph Tassarotti, Jean-Baptiste Tristan, Koundinya Vajjha

Share this with someone who'll enjoy it:

We present a machine-checked, formal proof of PAC learnability of the concept class of decision stumps. A formal proof has every step checked and justified using fundamental axioms of mathematics. We construct and check our proof using the Lean theorem prover. Though such a proof appears simple, a few analytic and measure-theoretic subtleties arise when carrying it out fully formally. We explain how we can cleanly separate out the parts that deal with these subtleties by using Lean features and a category theoretic construction called the Giry monad.

* 16 pages 

   Access Paper Source

Share this with someone who'll enjoy it: