4 ms·

Hypothesis: an LLM capable of generating a correct proof in a formal language, not through random chance but through whatever passes for “reasoning,” should als

Hypothesis: an LLM capable of generating a correct proof in a formal language, not through random chance but through whatever passes for “reasoning,” should also be capable of describing the proof in a way meaningful to humans. Because LLMs have a limited context window and are trained on human behavior, they will generate solutions similar to what humans would generate. We have already accepted some proofs we cannot fully understand, such as the proof of the four color theorem that used computational methods to explore a large solution space and demonstrate that no possible special-case combinations violate the theorem. But that was just one part of the proof. I wonder what we know about proof space generally, and if we had an ASI that reasoned in a substantially different way than humans, what types of proofs it would be likely to generate. Do most proofs contain structural components that humans find pleasing? Do most devolve into convoluted case analyses? Is there a simplest form that a set of correct proofs could be reduced to?

ndriscoll 2y ago
To me this seems obvious. Copilot might generate wrong things, but what I've seen tends to be human-readable. My experience with Lean is that it feels very much like a functional programming language like Scala, so I'd have to assume that a coding assistant that also knows Lean syntax/libraries would work just like any other programming language. There will perhaps need to be a transition period where we might need to look at basic type theory augmenting or replacing material in introductory proof classes. Instead of truth tables and ZFC, teach math-as-programming. Propositions are types, implications are functions, etc. If you have the right foundation, I think the stuff ends up being quite legible. Mathlib is very abstract which makes it harder to approach as a beginner, but you could imagine a sort of literate programming approach where we walk students through building their own personal Mathlib, refactoring it to use higher abstractions as they build it up, etc. In a sense this is what a math education is today, but with a kind of half-formal, half-natural language and with a bunch of implicit assumptions about what techniques the student really knows (since details are generally omitted) vs. letting them use whatever macros/tactics/theorems they've learned/created in other courses. This could all be especially powerful if the objects you're working with have good Widgets[0][1] so you could visualize and interact with various intermediate expressions. I see tons of potential here. The Lean games[2] also show the potential for a bright future here that's kind of along the lines of "build your own library around topic X" (the NN game has been posted here a few times, but it's actually a framework with other games too!). [0] https://lean-lang.org/lean4/doc/examples/widgets.lean.html https://lean-lang.org/lean4/doc/examples/widgets.lean.html [1] https://github.com/leanprover-community/ProofWidgets4/blob/main/doc/infoview-rbtree.png https://github.com/leanprover-community/ProofWidgets4/blob/m... [2] https://adam.math.hhu.de/ https://adam.math.hhu.de/

ndriscoll 2y ago

To me this seems obvious. Copilot might generate wrong things, but what I've seen tends to be human-readable. My experience with Lean is that it feels very much like a functional programming language like Scala, so I'd have to assume that a coding assistant that also knows Lean syntax/libraries would work just like any other programming language. There will perhaps need to be a transition period where we might need to look at basic type theory augmenting or replacing material in introductory proof classes. Instead of truth tables and ZFC, teach math-as-programming. Propositions are types, implications are functions, etc. If you have the right foundation, I think the stuff ends up being quite legible. Mathlib is very abstract which makes it harder to approach as a beginner, but you could imagine a sort of literate programming approach where we walk students through building their own personal Mathlib, refactoring it to use higher abstractions as they build it up, etc. In a sense this is what a math education is today, but with a kind of half-formal, half-natural language and with a bunch of implicit assumptions about what techniques the student really knows (since details are generally omitted) vs. letting them use whatever macros/tactics/theorems they've learned/created in other courses. This could all be especially powerful if the objects you're working with have good Widgets[0][1] so you could visualize and interact with various intermediate expressions. I see tons of potential here. The Lean games[2] also show the potential for a bright future here that's kind of along the lines of "build your own library around topic X" (the NN game has been posted here a few times, but it's actually a framework with other games too!). [0] https://lean-lang.org/lean4/doc/examples/widgets.lean.html https://lean-lang.org/lean4/doc/examples/widgets.lean.html [1] https://github.com/leanprover-community/ProofWidgets4/blob/main/doc/infoview-rbtree.png https://github.com/leanprover-community/ProofWidgets4/blob/m... [2] https://adam.math.hhu.de/ https://adam.math.hhu.de/