Stream: Machine Learning for Theorem Proving

Topic: Proof repair and constructive math

Jason Rute (Sep 10 2022 at 10:51):

I thought his was an interesting tweet thread:

Jason Rute (Sep 10 2022 at 10:51):

It is interesting from the standpoint of building AI for theorem proving of course.

Jason Rute (Sep 10 2022 at 10:51):

But I also thought the line "easier to reuse, repair, and generalize existing proofs to derive new proofs in constructive logics" was interesting. My (probably butchered) understanding is that Talia works on proof repair, the idea that we should be able automate fixing formal proofs if say the statement slightly changes or some downstream dependency changes. Their methods of automation (if I understand correctly) exploit purely constructive proofs which don't use the axiom of choice, the law of excluded middle, function extentionality, uniqueness of identity proofs, (nor even the univalence axiom). Now I don't know enough about this to understand the points, but I think it is an interesting discussion, since I'm sure Lean would like automated proof repair in the future, and Lean also relies heavily on some forms of classical logic (and has UIP built in).

Jason Rute (Sep 10 2022 at 10:51):

Of course Talia's work I think is more focused on formal verification than formal mathematics. Nonetheless, Lean 4 will also be very focused on formal verification of all the code written in Lean 4. Leo has said that few people, even those interested in Lean 4 for its formal verification abilities, find that constructive logic is that necessary, but I think it will be interesting to see how this plays out.

Jason Rute (Sep 10 2022 at 10:51):

Of course, it may be also that many proofs are constructive enough to easily repair since one doesn't go out of their way to jam in LEM where it doesn't naturally need to be, so I think it comes down to how essential constructive math is for proof repair.

Jason Rute (Sep 10 2022 at 11:07):

Or it may be that there are other forms of classical proof repair that just haven't be found yet. I think Talia's work was also focused on term proofs instead of tactic proofs (but I could be wrong). Terminal simps are one example of self-repairing tactics. Also, I still think that ML could go a long way in this area since it is really a question of making simple fixes to a proof which are obvious to say a human (and Talia seems to agree at least in part, given their current research focus). ML may blunt some of the constructive/classical, term-proof/tactic-proof pain, but maybe I'm being naive or overly optimistic. (I'd be interested in Talia's thoughts on this, but I think they run in different online forum circles. :smile: )

Kevin Buzzard (Sep 10 2022 at 11:39):

Talia's AITP talk starts at 2:57:30 or so at this video link.

Last updated: Dec 20 2023 at 11:08 UTC