AI Challenges

Here are the AITP bets from Josef Urban's 2014 talk at Institut Henri Poincare

See slide 34: Betting (Putting Money Where My Mouth Is)
  1. In 20 years, 80% of MML and Flyspeck toplevel theorems will be provable automatically (same hardware, same library versions as in 2014 - about 40% then)
  2. The same in 30 years - I'll give you 2:1, In 10 years: 60%
  3. In 25 years, 50% of the toplevel statements in LaTeX-written Msc-level math curriculum textbooks will be parsed automatically and with correct formal semantics
Tom Hales has offered to take additional bets if JU's 10k EUR limit runs out.

Betting done so far

Freek Wiedijk has bet JU on a slightly modified bet 3: it is about all statements in Proofs from the Book. This will be evaluated on June 21st, 2040, the judge is Robbert Krebbers, and the winner is entitled to a book worth 200 of year 2015 USD.