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: