Lean would be happy with this, and we could accept this if we’re feeling lenient. Let’s begin with a simple statement about groups. If it is incorrect, you can give the app feedback on what to fix in a natural, conversational way. If the generated formal statement is correct, fantastic! You can copy and past the statement into your Lean source file. The interface is straightforward: enter a theorem statement in good-old, and the app will have a go at formalizing it. Under the hood, these translation are generated by OpenAI’s Codex, a text generation model trained on Github source code. Recent advances in machine learning suggest such a system is not as far in the future as it may sound.Īs a very small step towards realizing this vision, myself and Edward Ayers have developed Lean Chat, a VS-code extension that provides an interface for autoformalizing natural language theorem statements in Lean.
#Coq definition code#
If we extrapolate this trend to its logical conclusion, we might imagine an interactive theorem prover where every single line of code is hidden behind the interface, and the user interacts with the machine purely in natural language. Today, there is still a learning curve to Lean, but once one learns the syntax, mathlib proofs are not terribly far from an informal version-at least compared to Automath.
Contemporary systems such as Coq and Isabelle add many useful features such as type classes and tactics, and most users don’t have to think about what the axioms even are. Mizar was the first attempt to make formal proofs comprehensible to mainstream mathematicians. Automath, the first interactive prover, floated very close to the axioms indeed. The history of interactive theorem proving can be told as a story of allowing the user to interact with the system at gradually higher levels of abstraction, getting further away from the axioms and closer to informal mathematics. He completed this work while visiting Carnegie Mellon’s Hoskinson Center for Formal Mathematics.
Zhangir is an undergraduate at Yale, majoring in computer science and mathematics. This is a guest post, written by Zhangir Azerbayev.
0 kommentar(er)
