We will integrate ALPHA with proof assistants such as Lean and Isabelle to ensure reliability of the proofs generated and to gain access to proof assistants’ extensive library and metaprogramming features while
leveraging connections with the Lean community through PIs Tao and Sottile.
Our approach builds on our strengths in PDE, analytic number theory, graph algorithms, tool-
augmented large language model (LLM), code generation, neurosymbolic AI, and automated the-
orem proving.
We will integrate ALPHA with proof assistants such as Lean and Isabelle to ensure reliability of the proofs generated and to gain access to proof assistants’ extensive library and metaprogramming features while
leveraging connections with the Lean community through PIs Tao and Sottile.
Our approach builds on our strengths in PDE, analytic number theory, graph algorithms, tool-
augmented large language model (LLM), code generation, neurosymbolic AI, and automated the-
orem proving.
PIs:
Copyright. All Rights Reserved.