Solving ~20% of all cases by brute force

Stream: Equational

[Vlad Tsyrklevich]

After proving a bunch of implications using brute force by trivial methods, I did some work on getting it ready to upstream. In particular, I wrote simple tools to compute the transitive reduction (e.g. minimal set of necessary implications) and transitive closure (e.g. how many total implications are implied by a set of implications) of a set of implications and found that I can prove 4.2m implications (just under 20% of 4694^2) using just 15,230 implications. Wikipedia says that computing the transitive reduction of a cyclic graph is in NP, so I'm using a hacked up approximate method to calculate that number, it should not be considered a maximal possible lower-bound. I've uploaded the first cut of the proofs in a PR here: https://github.com/teorth/equational_theories/pull/54 I will also upload the transitive reduction script when I clean it up, and I plan to fix some of the hacky theorems I generated (e.g. the try {}s bruteforcing different number of parameters)

[Vlad Tsyrklevich]

If you'd like to compute the transitive closure of the implications for this PR yourself, you can do using ruby scripts/transitive_closure.rb data/REDUCED.csv

[Nicholas Carlini]

Okay, this almost definitely supersedes my "just rename them" set of 50k. I just started a topic on how to format large generated merges. I think it makes sense to (1) put the code for generating the proofs near the generated proof, and (2) to make each generated lean file separate, so that it's reproducible and doesn't require merging files together.

[Nicholas Carlini]

https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/File.20structure.20for.20large.20auto-generated.20merges/near/473353745

[Vlad Tsyrklevich]

I've done some simple testing of the numbers I claim here, but additional verification would be welcome. In particular, I did check that the transitive closure of the implications in that PR do not overlap with Nicholas Carlini's refutations

[Nicholas Carlini]

(I don't know how to link to other messages.)

[Vlad Tsyrklevich]

Nicholas Carlini said:

Okay, this almost definitely supersedes my "just rename them" set of 50k. I just started a topic on how to format large generated merges. I think it makes sense to (1) put the code for generating the proofs near the generated proof, and (2) to make each generated lean file separate, so that it's reproducible and doesn't require merging files together.

You can calculate the transitive closure yourself if you'd like to check, after all, the actual number of theorems in the PR is 15k, and I'm not sure that mine are a strict superset of yours

[Vlad Tsyrklevich]

Nicholas Carlini said:

Okay, this almost definitely supersedes my "just rename them" set of 50k. I just started a topic on how to format large generated merges. I think it makes sense to (1) pu

Agreed on both counts. Unfortunately, the scripts I have for #1 right now are quite ugly, so one thing I will have to figure out what is what is worth upstreaming to allow reproducing it. It would be cool if I was good enough at lean to do it in a nice way using lean itself, instead of my "generate lean files, then make -j6 lean executing them, and then delete theorems with errors" method

[Daniel Weber]

Transitive closure is NP-complete? Do you mind linking to that wiki page? I'm fairly sure there's a simple $O(nm)$ algorithm of running DFS/BFS from every node

[Nicholas Carlini]

I would be in favor of just putting whatever code you have in this format and letting people clean it up as they'd like. The beauty of lean is that we know the proofs are correct regardless of how ugly the code that generated it was.

[Vlad Tsyrklevich]

Daniel Weber said:

Transitive closure is NP-complete? Do you mind linking to that wiki page? I'm fairly sure there's a simple $O(nm)$ algorithm of running DFS/BFS from every node

Oops, that should have been reduction, not closure. "Because of this difficulty, it is NP-hard to find the smallest subgraph of a given graph G with the same reachability (its minimum equivalent graph).[[3]]" from https://en.wikipedia.org/wiki/Transitive_reduction Note that it's specific to cyclic graphs.

[Vlad Tsyrklevich]

Finding the Hamiltonian cycle in the SCC is exactly the bit that I just shotgun away with an approximate method in my script but it seems to work fine. I couldn't find code that I wanted to use this for online, so I hacked something up myself with the aid of ChatGPT, but it seems to agree with the transitive closures I compute.

[Daniel Weber]

Because implications are transitively closed, I'm quite sure you can compute the condensation graph and then run transitive reduction on it

[Amir Livne Bar-on]

Greedy approximates within a factor of 2 though, right? Which is enough to reduce runtime from quadratic to linear

[Amir Livne Bar-on]

Also a Hamiltonian cycle would not be the easiest in some cases, e.g. it's very efficient to prove implications to/from Eq2

[Vlad Tsyrklevich]

Daniel Weber said:

Because implications are transitively closed, I'm quite sure you can compute the condensation graph and then run transitive reduction on it

Yes this is what I do, but what wikipedia notes is that when you uncondense to get the minimimal graph you need to find a hamiltonian in the SCCs which is what is hard, unless I'm misunderstanding

[Vlad Tsyrklevich]

Realistically, I think someone could write something that does this in a reasonable time given this data set size, I just used an approximate method to get around the hamiltonian calculation, hence, not providing a true lower bound.

[Daniel Weber]

Oh, there can be cases where your brute force proves a -> b and b -> c but not a -> c? You could always prove it by combining implications, but I guess that does somewhat remove the benefit of taking a transitive closure

[Vlad Tsyrklevich]

Daniel Weber said:

Oh, there can be cases where your brute force proves a -> b and b -> c but not a -> c? You could always prove it by combining implications, but I guess that does somewhat remove the benefit of taking a transitive closure

Yes, I was surprised by this as well actually and had not taken it into account, and then found that I had edges in my reduction that weren't in my original graph!

[Daniel Weber]

Interesting, do you happen to have a small example?

[Vlad Tsyrklevich]

Daniel Weber said:

Interesting, do you happen to have a small example?

[4379, 4377, 4373, 4372, 4368, 4366, 4365] form a cycle
egrep -e "^(4379|4377|4373|4372|4368|4366|4365),(4379|4377|4373|4372|4368|4366|4365)" IMPLICATION_*
IMPLICATION_apply_h.csv:4368,4365
IMPLICATION_apply_h.csv:4368,4366
IMPLICATION_apply_h.csv:4373,4372
IMPLICATION_apply_h.csv:4377,4365
IMPLICATION_apply_h.csv:4379,4365
IMPLICATION_apply_h.csv:4379,4366
IMPLICATION_apply_h.csv:4379,4368
IMPLICATION_apply_h.csv:4379,4372
IMPLICATION_apply_h.csv:4379,4373
IMPLICATION_apply_h.csv:4379,4377
IMPLICATION_repeated_rw.csv:4365,4366
IMPLICATION_repeated_rw.csv:4365,4368
IMPLICATION_repeated_rw.csv:4365,4372
IMPLICATION_repeated_rw.csv:4365,4373
IMPLICATION_repeated_rw.csv:4365,4377
IMPLICATION_repeated_rw.csv:4365,4379
IMPLICATION_repeated_rw.csv:4366,4365
IMPLICATION_repeated_rw.csv:4366,4368
IMPLICATION_repeated_rw.csv:4366,4372
IMPLICATION_repeated_rw.csv:4366,4373
IMPLICATION_repeated_rw.csv:4366,4377
IMPLICATION_repeated_rw.csv:4366,4379
IMPLICATION_repeated_rw.csv:4372,4365
IMPLICATION_repeated_rw.csv:4372,4366
IMPLICATION_repeated_rw.csv:4372,4368
IMPLICATION_repeated_rw.csv:4372,4373
IMPLICATION_repeated_rw.csv:4372,4377
IMPLICATION_repeated_rw.csv:4372,4379
IMPLICATION_repeated_rw.csv:4373,4366
IMPLICATION_repeated_rw.csv:4377,4372
IMPLICATION_repeated_rw.csv:4379,4365
IMPLICATION_repeated_rw.csv:4379,4366
IMPLICATION_repeated_rw.csv:4379,4368
IMPLICATION_repeated_rw.csv:4379,4372
IMPLICATION_repeated_rw.csv:4379,4373
IMPLICATION_repeated_rw.csv:4379,4377
IMPLICATION_repeated_rw_no_left_sym.csv:4365,4366
IMPLICATION_repeated_rw_no_left_sym.csv:4365,4368
IMPLICATION_repeated_rw_no_left_sym.csv:4365,4372
IMPLICATION_repeated_rw_no_left_sym.csv:4365,4373
IMPLICATION_repeated_rw_no_left_sym.csv:4365,4377
IMPLICATION_repeated_rw_no_left_sym.csv:4365,4379
IMPLICATION_repeated_rw_no_left_sym.csv:4366,4365
IMPLICATION_repeated_rw_no_left_sym.csv:4366,4368
IMPLICATION_repeated_rw_no_left_sym.csv:4366,4372
IMPLICATION_repeated_rw_no_left_sym.csv:4366,4373
IMPLICATION_repeated_rw_no_left_sym.csv:4366,4377
IMPLICATION_repeated_rw_no_left_sym.csv:4366,4379
IMPLICATION_repeated_rw_no_left_sym.csv:4368,4365
IMPLICATION_repeated_rw_no_left_sym.csv:4368,4366
IMPLICATION_repeated_rw_no_left_sym.csv:4372,4365
IMPLICATION_repeated_rw_no_left_sym.csv:4372,4366
IMPLICATION_repeated_rw_no_left_sym.csv:4372,4368
IMPLICATION_repeated_rw_no_left_sym.csv:4372,4373
IMPLICATION_repeated_rw_no_left_sym.csv:4372,4377
IMPLICATION_repeated_rw_no_left_sym.csv:4372,4379
IMPLICATION_repeated_rw_no_left_sym.csv:4373,4372
IMPLICATION_repeated_rw_no_left_sym.csv:4377,4365
IMPLICATION_repeated_rw_no_left_sym.csv:4379,4365
IMPLICATION_repeated_rw_no_left_sym.csv:4379,4366
IMPLICATION_repeated_rw_no_left_sym.csv:4379,4368
IMPLICATION_repeated_rw_no_left_sym.csv:4379,4372
IMPLICATION_repeated_rw_no_left_sym.csv:4379,4373
IMPLICATION_repeated_rw_no_left_sym.csv:4379,4377

but note that I only have 30 implications between them, not 7^2=49
egrep -e "^(4379|4377|4373|4372|4368|4366|4365),(4379|4377|4373|4372|4368|4366|4365)" IMPLICATION_* | cut -d ':' -f 2 |sort -u | wc -l
30

[Vlad Tsyrklevich]

I've marked https://github.com/teorth/equational_theories/pull/54 as ready for review. One thing I did not do here, is delete other theorems subsumed by these implications, e.g. in Subgraph.lean or other auto-generated implications. Should I? It would reduce the size of the repo, especially by making use of the transitive reduction, but I'm not sure if that's kosher or desirable. Input is welcome.

[Nicholas Carlini]

Which proof is "canonical"? On one hand "uses fewer proof techniques" is nice, on the other "simplest method to prove A=>B" is nice.

[Vlad Tsyrklevich]

Nicholas Carlini said:

Which proof is "canonical"? On one hand "uses fewer proof techniques" is nice, on the other "simplest method to prove A=>B" is nice.

Agreed. For these trivial proofs though, they are mostly functionally identical (all these proofs are just trivial rewrites.)

[Nicholas Carlini]

Yeah, it would just be good to have a way to do this that's semi-standard for future cases. I imagine, for example, that there will exist some powerful techniques that can prove things you could prove easier ways, and I don't know which should be the one that's retained for each method.

[Terence Tao]

I think if the manual proof is functionally identical to the automated proof then it would be fine (though not obligatory) to remove the manual proof and import the automated proof instead. This may complicate some future tooling a little bit though - for instance, if one wanted to use a tool to visualize all the implications between the equations studied in Subgraph.lean, and Subgraph.lean imports a massive generated file that mentions thousands of other equations, one would still only like to see the implications that came from the original file Subgraph.lean. But perhaps some suitable options can be set in such tools to allow this. EDIT: I guess the thing to do is allow for an option in such tools to restrict attention to the equations in Equations.lean (or some other specified set), regardless of how many lean files one imports.

On the other hand, as the subgraph gets larger, and the fraction of implications that are automatically verified increases, we certainly want to take advantage of the automation to make the human verification tasks easier. After all that's one of the major goals of this project, to figure out how to get humans and automated tools to work together smoothly!

[Vlad Tsyrklevich]

Hmm, on the CI I'm getting a stack overflow: https://github.com/teorth/equational_theories/actions/runs/11086264732/job/30803611966?pr=54 Perhaps Apply.lean, ~40k LOC is too large, I will try splitting it and see

[Shreyas Srinivas]

I reran the build. It shouldn't fail because I am building the same subproject successfully in another CI run for a different PR

[Vlad Tsyrklevich]

I'm not sure I understand, it's failing in my newly submitted code

[Shreyas Srinivas]

oh then its different

[Vlad Tsyrklevich]

Terence Tao said:

I think if the manual proof is functionally identical to the automated proof then it would be fine (though not obligatory) to remove the manual proof and import the automated proof instead. This may complicate some future tooling a little bit though - for instance, if one wanted to use a tool to visualize all the implications between the equations studied in Subgraph.lean, and Subgraph.lean imports a massive generated file that mentions thousands of other equations, one would still only like to see the implications that came from the original file Subgraph.lean. But perhaps some suitable options can be set in such tools to allow this. EDIT: I guess the thing to do is allow for an option in such tools to restrict attention to the equations in Equations.lean (or some other specified set), regardless of how many lean files one imports.

On the other hand, as the subgraph gets larger, and the fraction of implications that are automatically verified increases, we certainly want to take advantage of the automation to make the human verification tasks easier. After all that's one of the major goals of this project, to figure out how to get humans and automated tools to work together smoothly!

The mention of visualization made me think of something. In computing the transitive reduction of a large graph, I first need to 'condense' the graph, or combine all bi-implications (e.g. A->B->C->A) to a single node. This is exactly the operation we will have to do if we want to reduce the visualization size to make it comprehensible. However, even condensed, the current graph of the implications I am submitting has 3.6k vertices and 14k edges. That said, future additions could theoretically further increase the size of the strongly connected components and reduce the condensed graph size.

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

Terence Tao said:

I think if the manual proof is functionally identical to the automated proof then it would be fine (though not obligatory) to remove the manual proof and import the automated proof instead. This may complicate some future tooling a little bit though - for instance, if one wanted to use a tool to visualize all the implications between the equations studied in Subgraph.lean, and Subgraph.lean imports a massive generated file that mentions thousands of other equations, one would still only like to see the implications that came from the original file Subgraph.lean. But perhaps some suitable options can be set in such tools to allow this. EDIT: I guess the thing to do is allow for an option in such tools to restrict attention to the equations in Equations.lean (or some other specified set), regardless of how many lean files one imports.

On the other hand, as the subgraph gets larger, and the fraction of implications that are automatically verified increases, we certainly want to take advantage of the automation to make the human verification tasks easier. After all that's one of the major goals of this project, to figure out how to get humans and automated tools to work together smoothly!

The mention of visualization made me think of something. In computing the transitive reduction of a large graph, I first need to 'condense' the graph, or combine all bi-implications (e.g. A->B->C->A) to a single node. This is exactly the operation we will have to do if we want to reduce the visualization size to make it comprehensible. However, even condensed, the current graph of the implications I am submitting has 3.6k vertices and 14k edges. That said, future additions could theoretically further increase the size of the strongly connected components and reduce the condensed graph size.

With more implications I presume this will become a more interesting graph, for now it's still fairly chaotic. Squares are single equations, circles are strongly connected components, and the ones filled-in green are from Subgraph.lean
output.svg

[Terence Tao]

Nice image! You could upload it to the images folder and maybe add a link to it in README.md. At some point we may have a whole gallery of visuals, but for now anything is better than nothing.

[Terence Tao]

(I am looking forward to the "eye candy" phase of the project.)

[Andrii Kurdiumov]

I improve generate_image.py to be able include implications from all lean files, including generated one. Does that interesting enough to submit?

[Daniel Weber]

I think that's good, although it might be better to edit it to process the output of extract_implications.lean, to have the code responsible for that concentrated (in equational#102 I modify it to process multiple files, and after equational#29 is done it will also compute the transitive closure)

[Andrii Kurdiumov]

Seems to be I’m slightly behind all the time. Will take a look at your PRs to better understand how it’s done in Lean

[Andrii Kurdiumov]

Here the two pictures which I have

• All direct theorems All.png
  
• Transitive closure of all existing work.
  All_closure.png
  

[Daniel Weber]

image.png
These are interesting patterns. What is the order? Simply the numbers of the equations?

[Andrii Kurdiumov]

Yes, it is number of the equations,

[Joachim Breitner]

Beautiful :-)

[Vlad Tsyrklevich]

@Andrii Kurdiumov Cool! It would be interesting to graph non-implications too, though there are not currently many upstream in the repo, I could point you to where you could generate a huge number of them easily

[Vlad Tsyrklevich]

I assume the long lines across are the Eq 2 cluster, but no idea what the other visible structure is

[Andrii Kurdiumov]

Given that you guys love pictures. You can see how different methods of generated proving have structures.

RewriteHypothesis.png
RewriteHypothesisAndGoal.png
Apply.png
Apply2.png
RewriteGoal.png

[Andrii Kurdiumov]

It's barely visible in some cases, but still quite entertaining

[Andrii Kurdiumov]

@Vlad Tsyrklevich non-implications displayed in red, but there so small of them, so they are almost invisible. If you have something else in mind, let me know, I can take a look

[Daniel Weber]

Are you also computing the closure of non-implications, or only of implications?

[Joachim Breitner]

Andrii Kurdiumov said:

Vlad Tsyrklevich non-implications displayed in red, but there so small of them, so they are almost invisible. If you have something else in mind, let me know, I can take a look

I hope I’ll get to add plenty very soon :-)

[Andrii Kurdiumov]

@Daniel Weber just for the record. I only maintain script I would say. Originaly it was written not by me, I just happen to be interested in results.

Yes, for now only closure for implications calculated. I thinking about non-impovations but do not do it. Maybe that’s would be next step

[Vlad Tsyrklevich]

Andrii Kurdiumov said:

Vlad Tsyrklevich non-implications displayed in red, but there so small of them, so they are almost invisible. If you have something else in mind, let me know, I can take a look

There's a way to calculate the ones Joachim will add, but if Joachim thinks his change will land soon, probably better to just wait for it

[Jared green]

any idea if these matrix patterns can be derived/proven? do they have random outliers?

[Joachim Breitner]

Are these images already based on the output of extract_implications? If so, then on https://github.com/teorth/equational_theories/pull/130 you’ll have a few more anti-implications to display.