Just wanted to point out that using machine learning to produce formal proofs is not new; this work has been ongoing in both the machine learning and programming languages community. Most of the work has been done in the Coq or Isabelle/HOL proof languages, with a few things done in Lean. As far as I can tell, a lot of the other work is much farther along in terms of actually producing proofs of useful things; Proverbot9001 (proverbot9001.ucsd.edu), which uses Coq, is somewhere near proving 25% of the theorems in a verified compiler, a better example of th... (read more)
Just wanted to point out that using machine learning to produce formal proofs is not new; this work has been ongoing in both the machine learning and programming languages community. Most of the work has been done in the Coq or Isabelle/HOL proof languages, with a few things done in Lean. As far as I can tell, a lot of the other work is much farther along in terms of actually producing proofs of useful things; Proverbot9001 (proverbot9001.ucsd.edu), which uses Coq, is somewhere near proving 25% of the theorems in a verified compiler, a better example of th... (read more)