Proof repair and constructive math

Stream: Machine Learning for Theorem Proving

[Jason Rute]

I thought his was an interesting tweet thread:

• https://twitter.com/TaliaRinger/status/1568516530153062402
• https://twitter.com/TaliaRinger/status/1568516797435084800
• https://twitter.com/TaliaRinger/status/1568517033595404288

When it comes to classical versus constructive logics, I want to reiterate that I think automation is currently easier in the former only because historically, people working on automation have focused on taking advantage of the benefits the former offer, but not the latter

- Talia Ringer 🌻🪬 (@TaliaRinger)

There are deep tradeoffs between these logics that make it easier to synthesize proofs from scratch in classical logics, but easier to reuse, repair, and generalize existing proofs to derive new proofs in constructive logics

- Talia Ringer 🌻🪬 (@TaliaRinger)

It's in my view a mistake to approach automation the same way for both kinds of logics, rather than to build automation that exploits the strengths of each

- Talia Ringer 🌻🪬 (@TaliaRinger)

[Jason Rute]

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

[Jason Rute]

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]

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]

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]

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]

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