Demos, Presentations and Resources

Videos

• AI/ATP helping to prove Mizar goals in real time
• TacticToe proving HOL4 goals in real time
• Probabilistic/semantic system translating informal statements to formal and proving them in HOL Light
• QSynt : AI rediscovers the Fermat primality test
• Evolutionary development of a portfolio of strategies for E prover

Online Systems

• MizAR - Automated Reasoning for Mizar
• informal2formal parser with theorem proving trained on Flyspeck
• informal2formal parser with Mizar typechecking trained on Mizar
• HOL(y)hammer
• Growing collection of interesting ENIGMA proofs over Mizar and the announcement of 75% of the Mizar library proved automatically (July 26, 2021)
• Proofgold blockchain (by Blake Keiller) and its forum with many resources (Megalodon, surreal numbers, conjectures) by Chad Brown.

Repositories and Blogs

• AI4REASON Github repos - includes ENIGMA, BliStrTune, grackle, GRUNGE, etc.
• Thibault Gauthier's Github repos - includes TacticToe, OEIS synthesis, etc.
• Zar Goertzel's research blog posts
• Jan Jakubuv's Github repos - includes grackle, ENIGMA, etc.
• Martin Suda's Github repos - includes Deepire, etc.
• Josef Urban's Github repos - includes MPTP, MaLARea, BliStr, etc.

Talks and Presentations

• Can Computers Really Do Math? article describing the AI4REASON project published by the Sciencesquared.eu server of the European Research Council (ERC).
• J. Urban - AGI'18 keynote: No one shall drive us from the semantic AI paradise of computer-understandable math and science! (video and slides)
• J. Urban - Hales'60 conference: Kepler and Hales: Conjectures and Proofs, Dreams and their Realization
• B. Piotrowski - IJCAR'18: ATPBoost: Learning Premise Selection in Binary Setting with ATP Feedback
• Z. Goertzel - ITP'18: ProofWatch: Watchlist Guidance for Large Theories in E
• Q. Wang - CICM'18: First Experiments with Neural Translation of Informal to Formal Mathematics