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

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/