Kevin Lacker on AI-Assisted Theorem Proving and Acorn

Kevin Lacker discusses Acorn, an AI-assisted theorem prover that enhances the usability of mathematical proof generation. Acorn simplifies the proving process by allowing users to express their ideas naturally while the AI manages the intricate details of proof justification, contrasting with traditional systems that require exhaustive detail. Guillermo highlights the foundational role of axioms in mathematics and the historical context of theorem proving, referencing Turing's work on Turing machines and the mechanization of mathematics for proof verification.

Kevin shares his background in mathematics and software engineering, detailing his experiences with large language models (LLMs) and their application in solving math contests. He reflects on the challenges of formalizing results using Lean, which requires extensive tactical knowledge, leading to the development of Acorn. Acorn focuses solely on mathematical expression, making it more accessible and user-friendly. It provides visual feedback in a coding environment, indicating correctness and highlighting errors, streamlining the process of checking mathematical truths.

The conversation highlights the differences between theorem proving in Acorn and Lean, with Acorn allowing users to state truths without detailing every step. Acorn's AI is trained on its own mathematical library, providing real-time feedback and enhancing the user experience. Learning Acorn is presented as more accessible for mathematicians compared to strict programming languages, with feedback mechanisms guiding users through the proof process.

The mathematical library serves as a foundational resource, built on axioms from which AI can learn to enhance its theorem-proving capabilities. Current methods in theorem proving are discussed, including the use of inductive structures and basic axioms that lead to more complex mathematical constructs. The conversation also addresses the increasing volume of mathematical papers and the potential for AI to assist in processing them.

Concerns about the inclusion of "ugly proofs" and their potential complications are raised, emphasizing the importance of distinguishing between theorem statements and their proofs. AI's role in debugging is discussed, with the ability to identify poor-quality content. Acorn aims to be both beautiful and simple, with the goal of enabling AI to process numerous PDFs daily.

The speaker's motivation for engaging with Acorn was to prove cryptographic concepts and formally verify cryptographic papers. The complexity of formal verification in Lean makes Acorn a more appealing option for proving mathematical statements related to cryptography. The challenge of formal verification within Acorn involves creating a specification of the executing machine and demonstrating correctness through inductive types.

The conversation highlights the unpredictable advancements in theorem proving and formal verification, emphasizing the historical trade-off between the benefits of formal verification and the extra work it entails. Acorn is integrating AI into theorem proving, allowing users to write statements that the AI verifies, streamlining the justification process. Concerns about AI's limitations are raised, particularly regarding its ability to innovate and the risk of incorrectly asserting proofs.

The discussion also touches on the importance of trust in verifiers, drawing parallels to Acorn's trusted core. The capabilities of LLMs are acknowledged, with suggestions to analyze the work of top mathematicians to validate published mathematics. The potential of the Acorn library is discussed, with the possibility of it serving as an ultimate imitator or generating its own theorems, creating a self-reinforcing cycle of improvement.