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

• No betting: all this could be today done in 5 years with reasonable resources - I believe this technology is getting easy ("This problem is data-driven-AI-easy")
• Hurry up: I will only accept bets up to 10k EUR total (negotiable)

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.