Remaining unformalized theorems?

Stream: Equational

[Mario Carneiro]

What is the status of the theorems that have been worked out on paper but not yet in lean? It might be nice to have some regular reporting and encouragement to work on these theorems too, not just the new mathematical work.

[Shreyas Srinivas]

Doesn't the equation explorer and dashboard only report the formalised theorems?

[Mario Carneiro]

Terry's blog posts have included both the number of unformalized implications and the number of unproven implications. Currently they are at 202 / 14, which suggests that formalization is lagging behind, although the exact number of manual theorems to prove to make the 202 reduce to 14 is not clear to me. (Of course it is less than 202-14 because some of those implications imply others.)

[Mario Carneiro]

Actually I guess this is the 66 "explicitly proven" theorems

[Mario Carneiro]

Which means that 82% of the work is already ready to go and doesn't even need new mathematical insights

[Shreyas Srinivas]

The statistics come from the equation explorer

[Mario Carneiro]

I'm not asking a technical question here. I'm trying to encourage work on this neglected part of the project

[Amir Livne Bar-on]

I think a lot of them are duals of proven theorems, so they're blocked on https://github.com/teorth/equational_theories/issues/147

[Mario Carneiro]

I thought that the definition of "implicitly proven" was being a transitive chain of possible duals of explicitly proven theorems?

[Mario Carneiro]

so all dual theorems should count as implicitly proven

[Amir Livne Bar-on]

Yes, you're right. I mixed them up.

[Amir Livne Bar-on]

Summarizing what I can see from the Github issues:

• There are 12 issues for formalizing proofs that are conveyed in Zulip or in the blueprint: #506, #516, #607, #633, #643, #660, #661, #663, #659, #666, #675, #762 (each for non-implications from a single equation)
• Two are currently claimed
• Some of the other issues were claimed and then disclaimed, some with significant progress in formalization
• Equations 713, 1289, 1447 remain, these don't have tickets linked to them, and the Equation Explorer comments refer to discussion on the difficulty of formalizing them

[Mario Carneiro]

713, 1289, 1447 don't seem to have reproducibility data, perhaps @Daniel Weber can comment on what they look like

[Mario Carneiro]

@Amir Livne Bar-on is that the complete list?

[Mario Carneiro]

it still seems like it wouldn't add to 66

[Amir Livne Bar-on]

There are 15 different equations on the LHS, at least in theory all the proofs of non-implications from each equation should be extremely similar

[Mario Carneiro]

hm, this list still seems a bit unclear regarding which subset of these is minimal to imply the rest

[Amir Livne Bar-on]

Just checked locally, I have 65 "explicit conjecture"s, and the only implications between them are within LHS class. The minimal set of non-implications to formalize is

Equation63 => Equation1692
Equation73 => Equation99
Equation73 => Equation203
Equation73 => Equation255
Equation73 => Equation4380
Equation713 => Equation359
Equation713 => Equation817
Equation713 => Equation1426
Equation713 => Equation3862
Equation854 => Equation413
Equation879 => Equation4065
Equation917 => Equation1629
Equation917 => Equation1729
Equation917 => Equation2441
Equation917 => Equation2541
Equation1076 => Equation3
Equation1289 => Equation2507
Equation1447 => Equation1431
Equation1447 => Equation4269
Equation1516 => Equation1489
Equation1518 => Equation47
Equation1518 => Equation614
Equation1518 => Equation817
Equation1518 => Equation3862
Equation1526 => Equation1223
Equation1526 => Equation2744
Equation1692 => Equation23
Equation1692 => Equation47
Equation1692 => Equation1832
Equation1722 => Equation1832
Equation1722 => Equation2644
Equation1722 => Equation3050
Equation3308 => Equation3511

[Mario Carneiro]

I count 33 implications, making progress already :)

[Terence Tao]

Thanks for taking the lead on this. I’m traveling for the next few days and will be disengaging somewhat during this time so it is great that you have collected this data.

one could perhaps prune Conjectures.lean with this new list. (A cheap way to make some nominal progress on the dashboard.)

[Terence Tao]

Also presumably many of the greedy algorithm arguments needed to do the formalization could benefit from mario’s new abstract greedy algorithm lemma

[Terence Tao]

Actually i have enough time to update conjectures.lean myself tonight, let me go ahead and do that

[Terence Tao]

created equational#771 for the three equations with very large proofs

[Mario Carneiro]

I am concerned with this one that the issue is not actionable without additional information. How many other conjectures are in that position, where a formalizer with too much time on their hands still can't do the job because it relies on unpublished data?

[Terence Tao]

That's the only one where there isn't a human readable proof. I guess @Daniel Weber can weigh in on what to do with this task.

[Daniel Weber]

Mario Carneiro said:

713, 1289, 1447 don't seem to have reproducibility data, perhaps Daniel Weber can comment on what they look like

They have a ruleset in https://github.com/teorth/equational_theories/tree/main/data/forcing_rules, but Vampire needs a SAT solver as a substep for proving their validity, so I'm unsure about that

[Daniel Weber]

It is possible that some settings and giving it enough time would let it prove it without that, and then the existing automated formalization could work, I don't know

[Terence Tao]

Incidentally, @Amir Livne Bar-on 's list isn't quite the right minimal set here, as it gives anti-implications to the weakest conclusions when instead it should be to the strongest conclusions. This particularly impacts 1076 that has a single weakest conclusion 3 but 22 maximal conclusions. As such, the number of explicit conjectures didn't actually get pruned that much: I think we end up with 57 statements to formalize, so only down slightly from 66. (There should be an accurate count by tomorrow morning; right now it's still going through CI, so the dashboard is temporarily off.)

[Mario Carneiro]

There are already a number of vampire proofs in lean currently, I'm not sure how they were generated but they use some translation of the superposition steps

[Vlad Tsyrklevich]

That's Daniel's doing.

[Shreyas Srinivas]

There is a thread where @Michael Bucko posted a pdf about this pipeline

[Shreyas Srinivas]

Here: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Vampire.20-.3E.20Lean/near/478147138

[Michael Bucko]

(keep in mind that this pdf should be updated based on the feedback from others -- in the same chat; it helped me understand how to work with Vampire though)