Markus Anders, who wrote the symmetry breaking system (satsuma) they use for SAT is pretty much a genius. His version of Kissat won the SAT Competition this year, with satsuma of course:
See slide 18. It was really nice to see him win. I have always been a huge fan of symmetry breaking, CryptoMiniSat (that I develop) had a symmetry breaking system, BreakID (which is _way_ slower than Markus' satsuma), in it for many years now.
I love SAT solver papers, always interesting to see auxiliary variable techniques, since those aren't really listed anywhere central
here for example, instead of saying {f(x,y,z)==g(x,y,z)}, authors instead make variable group a_w:=(f(x,y,z)=w||g(x,y,z)=w), and then apply "at most 1" to it. Can't be unequal if both functions only can have 1 result in total
this adds an index to iterate over, but separates internal subexpressions of f() and g(), removing 2 indixes (in this problem) and thus dropping whole power of n of clauses
---
what I don't get is that they aren't searching Tarski's problem per se, but for one specific solution to it (one identity that isn't resulting from given). I'd totally look for arithmetic models that violate expectations in other ways than Wilkie
Indeed, having a different "exotic identity" that has smaller countermodels would be awesome. Unfortunately, we tried a few alternatives to Wilkies and didn't find smaller countermodels.
Note that it's not obvious at all how to search the space of possible exotic identities, so a potential direction for future work would be to have a loop in which LLMs (perhaps through something like AlphaEvolve) propose an exotic identity, and then a SAT call tries to find a small countermodel. A big issue though, is that even with our efficient encoding the SAT calls would take at least a few minutes, so we wouldn't be able to afford testing millions of candidates. But if there were 1000 candidates that could potentially be tested...
(I'm one of the authors of the paper, thanks for the coment!).
> we tried a few alternatives to Wilkies and didn't find smaller countermodels.
I wish you spent at least a couple words in the paper about that. Even negative results are worth documenting! (even if you didn't get up to size 11, I'd've loved to hear about those other alternatives)
---
by the way, you mentioned that decreasing HSI6/10 from O(n^6) to O(n^5) clauses was slower - how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?
---
also, have you tried reordering order of operations in symmetry break? how much did it affect the search? I wonder if unique multiplication table might've been of help had it been disambiguated stronger (or weaker)
Man I wish I understood anything you said, or anything in tfa. Math has to have my personal gold medal for highest desire to learn coupled with total unwillingness to.
in a sense it's about a game. or... maybe it's better to call it a "challenge"
Tarski said "hey, what if we limit ourself only to positive integers? subtraction/division doesn't always work, so let's get rid of it. What can we say about +^? there are some obvious properties, like x+y=y+x for whatever x and y. Is that enough to describe all the equalities?".
Wilkie answered No, and a whole different hunt began - trying to find a set of pseudo "numbers" with pseudo "+^", that would have the same obvious properties, but not the non-obvious one
and SAT-solving is essentially asking computer to find things by describing what they are not - "1+2 is not invalid and can't be 2 different values", "1+(1+1) must not differ from (1+1)+1". A lot of such properties are easily expressible as "not the opposite" - but devil's in the details and some choices of opposites are faster for computer than others. Also symmetries are evil :)
They use the properties of Wilkie's counterexample to restrict the search space. So you can't just pick arbitrary identities that hold over the positive integers and repeat the process until you've found a smaller model.
I'm one of the authors of the arXiv paper. Thanks for bringing this to our attention! We were fully unaware of this repository, and it unfortunately did not come up during our literature search. Our approaches to the lower bound are pretty similar, although some technical differences make ours more efficient. For example, to show that there is no counterexample of size 10, we generate a formula with ~50k variables and ~2.7M clauses, which takes about 85 seconds to solve with Kissat. The encoder from this repository generates a formula with ~2k variables and ~33M clauses, which takes about 50 minutes to solve. We have sent an email to the authors of the Zenodo artifact to decide how to proceed!
Why is subtraction not part of the algebra? It’s certainly familiar to every high school math student. This omission allows the counterexample, so the reveal is a bit of a disappointment IMHO.
Subtraction is not closed over positive integers, which is untidy. The point of Tarski’s conjecture was to propose a minimal number of axioms and operations, AFAICS they define the standard semiring of positive integers (with the natural definition of exponentiation added).
(Edit: positive integers aren’t exactly a semiring because 0 is excluded, although some authors do define a semiring without the requirement of an additive identity element.)
If subtraction is allowed but negative numbers are not, that's known to be undecidable, even without exponentiation. There are several ways to deal with a subtraction with a negative result, but each variant is undecidable.
If we allow negatives but disallow exponentiation, that's decidable. If we allow negatives and partial exponentiation that stays within the integers, that's undecidable again.
If you allow negative integers, you get negative exponents. To accomodate negative exponents, you can expand the domain again, to rational numbers. If you allow rational numbers, then you have to allow rational exponents, which means you can take arbitrary nth roots. Which you could do, but now you're most of the way to the complex numbers (plus roots aren't unique anymore).
I'm not sure, but maybe it is due to that the expression a - b can be replaced as a + (-b)?
Similarly, I think a * b and a / b can be replaced with the same trick, but then I realized it may not work on non-abelian, or where multiplicative inverse is not available...
The subtraction point is interesting but I don't think it makes the result disappointing. The whole point of Tarski's problem is what follows from that very restricted set of elementary identities so finding the exact minimum countermodel under those rules still seems like a pretty satisfying result.
No, Gödel's incompleteness theorem applies to theories that can interpret first-order arithmetic, which includes quantified statements like "for all x, there exists a prime p > x".
In this case, we have the much simpler equational theory of positive integers under addition, multiplication, and exponentiation, which does not include any quantifiers. In fact, Gurevič showed that this theory is decidable [0]. On the other hand, Gurevič later showed that this theory is not finitely axiomatizable [1], so an infinite (but still computable) set of axioms is needed to fully characterize the theory.
Not using a set of axioms written in the original signature, of equations using the three operations and the constant 1. It's certainly possible to come up with a finite description of the true sentences in the theory, but only by extending the signature or using some method of description other than a set of axioms.
Yeah as someone that doesn't participate in a bunch of math stuff, I was really confused because it mentions SAT and High School algebra, but isn't about High School SAT testing at all.
They address the following concern of Zhang (2005), which contained prior work involving similar techniques:
> […] Of course, this conclusion is not proved mathematically. It is possible that the programs have some bugs, or the user (myself made some errors.
They address it as follows:
> We address this [… through] ChatGPT 5.5 Pro, through Codex, to automatically generate a Lean formalization that we then checked ourselves to confirm the statements and definitions indeed match their expected semantics. This process took multiple iterations and discussions with the model over several days, and generated over 10,000 lines of code.
This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect. I’m sure the result is correct, however I am deeply uncomfortable with this being mankind’s new mathematical process. Similar concerns have been expressed since the days of the 4 color theorem, but this feels different. Perhaps it is just new.
>in a nutshell, it defines an executable function encode that takes a natural number n ≥ 5 and emits a CNF formula, which is byte-for-byte equal to the output of our Python encoding
The phrase “byte-for-byte equal” makes my eye twitch these days.
Hi! One of the authors here. Whether checking the LLM-generated Lean statements/definitions is easy or not depends heavily on the area of mathematics and the concrete definitions at play. In this case it was remarkably easy. As you can see in the repository, the definition of a countermodel is easy to parse, and the statement corresponding to their nonexistence for n <= 11 is also very easy to check. If you have any questions regarding them, I would be happy to answer them.
Personally, this is one of the cases with LLM-generated Lean that I feel most comfortable with: the proofs are all mathematically simple, and we included an example of correctness for one of the SAT constraints in the paper to show that there is nothing complicated about them. Writing them all in Lean, however, would be a very tedious task for which I see no particular benefit (i.e., it's not like some other formalization projects in which one learns something by formalizing; for an example of a human-written Lean correctness proof of a SAT encoding, you can check the paper https://arxiv.org/abs/2403.17370 in which I participated).
Regarding the byte-for-byte equality, the point is that we first had the Python code (which we wrote manually), and then asked LLMs to implement an encoder in Lean that would not only produce "equivalent" formulas but exactly equal formulas, meaning that it would use the same variable indices and the same clauses in the same order. It is well-known that such superficial factors (e.g., clause or variable ordering) can actually have large effects on solver performance (see https://www.cs.utexas.edu/~marijn/publications/pos18.pdf). The Python code is not part of the trust chain, and the Lean code does not rely on it in any way. We included the Python code in the repository since it's much shorter and easier to read.
> This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect.
With https://en.wikipedia.org/wiki/Lean_(proof_assistant) (and other proof assistants), you need to review only the lines that correspond to the theorem that you want to prove and their types (I am not very experienced when it comes to lean, but I would assume that comes down to a few hundred lines of code, at most). The rest is left to typechecking (which, I would expect many in the field to agree, is at as reliable than your average peer review process in professional mathematics, and likely much more). That's the reason why Lean4 is making such a fuzz now.
That itself is not trivial too, but way easier than reviewing every function and definition used to prove that the theorems have indeed the types they claim.
If one accepts the proof of the https://en.wikipedia.org/wiki/Four_color_theorem, then there should not be new reservations these proofs; except from the maybe new additional failure scenario that the authors (still correctly!) proved theorems that don't state what they think they stated.
To sum it up: There is IMO no domain more suited for using LLMs than mathematical proofs that can be formalized using Lean4. The fact the hype-circle started earlier in software than in maths is due to the difference in monetary incentives I would assume. (Or another, rather radical and not really serious phrasing: "When it comes to Lean4 proofs that typechecks, there is no AI slop" - the theorem being proven might be uninteresting, but the proof itself is very very very very likely to be correct)
> “byte-for-byte equal”
The term itself or its association with LLMs? I would get the latter, if its the former: It's an desirable property to have, I always like seeing people going that far (assuming obviously that they indeed did so, and in the places where it matters!)
> you need to review only the lines that correspond to the theorem that you want to prove and their types
This is (unfortunately) not actually the case—just a few weeks ago, someone "proved" the Collatz conjecture via a Lean proof 1) whose theorem statement was correct, 2) typechecked, and 3) was even verified by external tools with their own implementations of the kernel.[0]
The problem was (AFAIK) that the Lean kernel has a lot of fancy features that aren't yet perfectly understood from a type-theoretic perspective (I don't think Lean is unique in this regard; pretty sure Rocq and Agda are in a similar situation). And so when the kernel implements some feature whose soundness isn't guaranteed, the independent verification tools (or at least some of them) follow suit, and now any issues in the former affect the latter as well.
Huh. Thanks for bringing that into my attention, and the link!
Yes, in hindsight it makes sense that a eager LLM would exploit bugs in the kernel itself. I have not read the details yet (but want to!) and assume that it is rather related to the layers directly before or after the type-theory core; i.e. that the AI managed to get a correct typecheck by sidestepping a check during in one of the translation steps somehow, by manipulating the kernels result or by going totally hacker mode and swap implementation/overwrite memory; that is just speculation on my part though, I mainly base if on what I know about Haskell and the https://en.wikipedia.org/wiki/Calculus_of_constructions in general that have not that many constructs, and I would assume the variants used in Rocq and Lean are proven sound.
For experimental features where soundness is not proven, all bets are off IMO, but of course, that does not stop bad actors from engagement knowlingly abusing unsoundness for their own gain. Fortunately, that kind of manipulation is easy to verify when one has access to the codebase; I am would assume that something like lints for experimental features exist, or better even, something like a "sound mode". That does not help against hacking the kernel machinery though.
Concluding notes:
- In this particular instance, the Collatz conjecture was appearently chosen on purpose to demonstrate the Kernel bug, from the same thread: "Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem."
- IF the code is made public (and it would be highly suspicious if parts of a proof where hidden), then I would assume this kind of hack is 1) easier to spot that other kinds of hack, since the asset-under-attack is really small and 2) there is not so much incentive to use much time/ingenuity/tokens on finding those hacks (the more are found and fixed, the better of course) 3) and they should be easy to defend against, I would assume; my first thought would be the flag I mentioned above that simply forbids all non-sound features, at the cost of limiting expressive power.
----
Edit: I checked, and I think it alleviates my worries in the sense that the bug(s) where not in the type theory or its implementation, but rather the machinery around it. Further context below:
The following is from that thread or links from it:
- "Fixes two things: (1) more strict/nuanced handling for structure/proj interactions, and (2) adds methods for enforcing that generated auxiliary data for inductives, constructors, and recursors are more strictly checked against the assertions in the export file." | That is the fix to the non-Lean-kernel that was mentioned. To me, (2) looks firmly like what I meant with "supporting machinery", regarding (1), I do not know enough to have an opinion about it (i.e. how on what layer those interactions happen(ed)) | https://github.com/ammkrn/nanoda_lib/pull/22
- "For example, pipeline wedges (execute this instruction and the core freezes and never executes another instruction) would not be found by these techniques..." | Power and limits of Lean | https://infosec.exchange/@david_chisnall/117003914014196496
- "@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it. There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer." | Computer-checked proofs run on computers, which brings its own attack vectors, independent of how well the kernel is written | https://infosec.exchange/@0xabad1dea/117002712346315184
personal, cautios takeaway after reading the details: If you use Lean4 to write proofs, or read that a reputable group of mathematicians publizised a Lean4 proof, you are still highly unlikely to be fooled by a bug, and if Fable 5 decides to exploit a 0day in the core Lean4 machinery, that should still be able to be caught quickly.
Markus Anders, who wrote the symmetry breaking system (satsuma) they use for SAT is pretty much a genius. His version of Kissat won the SAT Competition this year, with satsuma of course:
https://satcompetition.github.io/2026/downloads/satcomp26sli...
See slide 18. It was really nice to see him win. I have always been a huge fan of symmetry breaking, CryptoMiniSat (that I develop) had a symmetry breaking system, BreakID (which is _way_ slower than Markus' satsuma), in it for many years now.
I love SAT solver papers, always interesting to see auxiliary variable techniques, since those aren't really listed anywhere central
here for example, instead of saying {f(x,y,z)==g(x,y,z)}, authors instead make variable group a_w:=(f(x,y,z)=w||g(x,y,z)=w), and then apply "at most 1" to it. Can't be unequal if both functions only can have 1 result in total
this adds an index to iterate over, but separates internal subexpressions of f() and g(), removing 2 indixes (in this problem) and thus dropping whole power of n of clauses
---
what I don't get is that they aren't searching Tarski's problem per se, but for one specific solution to it (one identity that isn't resulting from given). I'd totally look for arithmetic models that violate expectations in other ways than Wilkie
Indeed, having a different "exotic identity" that has smaller countermodels would be awesome. Unfortunately, we tried a few alternatives to Wilkies and didn't find smaller countermodels.
Note that it's not obvious at all how to search the space of possible exotic identities, so a potential direction for future work would be to have a loop in which LLMs (perhaps through something like AlphaEvolve) propose an exotic identity, and then a SAT call tries to find a small countermodel. A big issue though, is that even with our efficient encoding the SAT calls would take at least a few minutes, so we wouldn't be able to afford testing millions of candidates. But if there were 1000 candidates that could potentially be tested...
(I'm one of the authors of the paper, thanks for the coment!).
> we tried a few alternatives to Wilkies and didn't find smaller countermodels.
I wish you spent at least a couple words in the paper about that. Even negative results are worth documenting! (even if you didn't get up to size 11, I'd've loved to hear about those other alternatives)
---
by the way, you mentioned that decreasing HSI6/10 from O(n^6) to O(n^5) clauses was slower - how big was the slowdown and how much less total clauses were there in that encoding? if I understand it correctly, that was still the biggest clause maker, but by how much?
---
also, have you tried reordering order of operations in symmetry break? how much did it affect the search? I wonder if unique multiplication table might've been of help had it been disambiguated stronger (or weaker)
Man I wish I understood anything you said, or anything in tfa. Math has to have my personal gold medal for highest desire to learn coupled with total unwillingness to.
in a sense it's about a game. or... maybe it's better to call it a "challenge"
Tarski said "hey, what if we limit ourself only to positive integers? subtraction/division doesn't always work, so let's get rid of it. What can we say about +^? there are some obvious properties, like x+y=y+x for whatever x and y. Is that enough to describe all the equalities?".
Wilkie answered No, and a whole different hunt began - trying to find a set of pseudo "numbers" with pseudo "+^", that would have the same obvious properties, but not the non-obvious one
and SAT-solving is essentially asking computer to find things by describing what they are not - "1+2 is not invalid and can't be 2 different values", "1+(1+1) must not differ from (1+1)+1". A lot of such properties are easily expressible as "not the opposite" - but devil's in the details and some choices of opposites are faster for computer than others. Also symmetries are evil :)
They use the properties of Wilkie's counterexample to restrict the search space. So you can't just pick arbitrary identities that hold over the positive integers and repeat the process until you've found a smaller model.
The lower bound had already been established in prior work: https://zenodo.org/records/18568303
I'm one of the authors of the arXiv paper. Thanks for bringing this to our attention! We were fully unaware of this repository, and it unfortunately did not come up during our literature search. Our approaches to the lower bound are pretty similar, although some technical differences make ours more efficient. For example, to show that there is no counterexample of size 10, we generate a formula with ~50k variables and ~2.7M clauses, which takes about 85 seconds to solve with Kissat. The encoder from this repository generates a formula with ~2k variables and ~33M clauses, which takes about 50 minutes to solve. We have sent an email to the authors of the Zenodo artifact to decide how to proceed!
I think you are right, it's weird that the paper doesn't mention it
Why is subtraction not part of the algebra? It’s certainly familiar to every high school math student. This omission allows the counterexample, so the reveal is a bit of a disappointment IMHO.
Subtraction is not closed over positive integers, which is untidy. The point of Tarski’s conjecture was to propose a minimal number of axioms and operations, AFAICS they define the standard semiring of positive integers (with the natural definition of exponentiation added).
(Edit: positive integers aren’t exactly a semiring because 0 is excluded, although some authors do define a semiring without the requirement of an additive identity element.)
Well, yes, but negative numbers are also well known to every high school math student.
Sure. But "High School Algebra (Excluding Subtraction) Problem" isn’t as catchy a name.
They subtracted the subtraction exclusion in the name of simplicity?
If subtraction is allowed but negative numbers are not, that's known to be undecidable, even without exponentiation. There are several ways to deal with a subtraction with a negative result, but each variant is undecidable.
If we allow negatives but disallow exponentiation, that's decidable. If we allow negatives and partial exponentiation that stays within the integers, that's undecidable again.
Because subtraction is not a total operation on positive integers. Negative numbers leave the domain.
Why was it important to Tarski to limit the domain to positive integers? That seems pointlessly arbitrary.
Truly, you could say that about many conjectures, especially more “fun” classical ones.
If you allow negative integers, you get negative exponents. To accomodate negative exponents, you can expand the domain again, to rational numbers. If you allow rational numbers, then you have to allow rational exponents, which means you can take arbitrary nth roots. Which you could do, but now you're most of the way to the complex numbers (plus roots aren't unique anymore).
I'm not sure, but maybe it is due to that the expression a - b can be replaced as a + (-b)?
Similarly, I think a * b and a / b can be replaced with the same trick, but then I realized it may not work on non-abelian, or where multiplicative inverse is not available...
We’re in the semiring of positive integers, so there are no additive (or multiplicative) inverses.
The subtraction point is interesting but I don't think it makes the result disappointing. The whole point of Tarski's problem is what follows from that very restricted set of elementary identities so finding the exact minimum countermodel under those rules still seems like a pretty satisfying result.
Isn't the underlying question proved impossible by Godel's incompletness theorem?
No, Gödel's incompleteness theorem applies to theories that can interpret first-order arithmetic, which includes quantified statements like "for all x, there exists a prime p > x".
In this case, we have the much simpler equational theory of positive integers under addition, multiplication, and exponentiation, which does not include any quantifiers. In fact, Gurevič showed that this theory is decidable [0]. On the other hand, Gurevič later showed that this theory is not finitely axiomatizable [1], so an infinite (but still computable) set of axioms is needed to fully characterize the theory.
[0] R. Gurevič, Equational theory of positive numbers with exponentiation, 1985, https://doi.org/10.2307/2044966
[1] R. Gurevič, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, 1990, https://doi.org/10.1016/0168-0072(90)90049-8
Not finitely axiomatizable using first-order logic, I assume.
Not using a set of axioms written in the original signature, of equations using the three operations and the constant 1. It's certainly possible to come up with a finite description of the true sentences in the theory, but only by extending the signature or using some method of description other than a set of axioms.
I thought SAT like the high school admissions test
Yeah as someone that doesn't participate in a bunch of math stuff, I was really confused because it mentions SAT and High School algebra, but isn't about High School SAT testing at all.
Sorry that people downvoted you rather than lending you a hand. You might find this useful as a place to start: https://pmc.ncbi.nlm.nih.gov/articles/PMC9464179/
They address the following concern of Zhang (2005), which contained prior work involving similar techniques:
> […] Of course, this conclusion is not proved mathematically. It is possible that the programs have some bugs, or the user (myself made some errors.
They address it as follows:
> We address this [… through] ChatGPT 5.5 Pro, through Codex, to automatically generate a Lean formalization that we then checked ourselves to confirm the statements and definitions indeed match their expected semantics. This process took multiple iterations and discussions with the model over several days, and generated over 10,000 lines of code.
This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect. I’m sure the result is correct, however I am deeply uncomfortable with this being mankind’s new mathematical process. Similar concerns have been expressed since the days of the 4 color theorem, but this feels different. Perhaps it is just new.
>in a nutshell, it defines an executable function encode that takes a natural number n ≥ 5 and emits a CNF formula, which is byte-for-byte equal to the output of our Python encoding
The phrase “byte-for-byte equal” makes my eye twitch these days.
Hi! One of the authors here. Whether checking the LLM-generated Lean statements/definitions is easy or not depends heavily on the area of mathematics and the concrete definitions at play. In this case it was remarkably easy. As you can see in the repository, the definition of a countermodel is easy to parse, and the statement corresponding to their nonexistence for n <= 11 is also very easy to check. If you have any questions regarding them, I would be happy to answer them.
Personally, this is one of the cases with LLM-generated Lean that I feel most comfortable with: the proofs are all mathematically simple, and we included an example of correctness for one of the SAT constraints in the paper to show that there is nothing complicated about them. Writing them all in Lean, however, would be a very tedious task for which I see no particular benefit (i.e., it's not like some other formalization projects in which one learns something by formalizing; for an example of a human-written Lean correctness proof of a SAT encoding, you can check the paper https://arxiv.org/abs/2403.17370 in which I participated).
Regarding the byte-for-byte equality, the point is that we first had the Python code (which we wrote manually), and then asked LLMs to implement an encoder in Lean that would not only produce "equivalent" formulas but exactly equal formulas, meaning that it would use the same variable indices and the same clauses in the same order. It is well-known that such superficial factors (e.g., clause or variable ordering) can actually have large effects on solver performance (see https://www.cs.utexas.edu/~marijn/publications/pos18.pdf). The Python code is not part of the trust chain, and the Lean code does not rely on it in any way. We included the Python code in the repository since it's much shorter and easier to read.
> This is extremely unconvincing. Manual review of 10,000 lines of AI generated code is a terrifying prospect.
With https://en.wikipedia.org/wiki/Lean_(proof_assistant) (and other proof assistants), you need to review only the lines that correspond to the theorem that you want to prove and their types (I am not very experienced when it comes to lean, but I would assume that comes down to a few hundred lines of code, at most). The rest is left to typechecking (which, I would expect many in the field to agree, is at as reliable than your average peer review process in professional mathematics, and likely much more). That's the reason why Lean4 is making such a fuzz now.
That itself is not trivial too, but way easier than reviewing every function and definition used to prove that the theorems have indeed the types they claim.
If one accepts the proof of the https://en.wikipedia.org/wiki/Four_color_theorem, then there should not be new reservations these proofs; except from the maybe new additional failure scenario that the authors (still correctly!) proved theorems that don't state what they think they stated.
To sum it up: There is IMO no domain more suited for using LLMs than mathematical proofs that can be formalized using Lean4. The fact the hype-circle started earlier in software than in maths is due to the difference in monetary incentives I would assume. (Or another, rather radical and not really serious phrasing: "When it comes to Lean4 proofs that typechecks, there is no AI slop" - the theorem being proven might be uninteresting, but the proof itself is very very very very likely to be correct)
> “byte-for-byte equal”
The term itself or its association with LLMs? I would get the latter, if its the former: It's an desirable property to have, I always like seeing people going that far (assuming obviously that they indeed did so, and in the places where it matters!)
> you need to review only the lines that correspond to the theorem that you want to prove and their types
This is (unfortunately) not actually the case—just a few weeks ago, someone "proved" the Collatz conjecture via a Lean proof 1) whose theorem statement was correct, 2) typechecked, and 3) was even verified by external tools with their own implementations of the kernel.[0]
The problem was (AFAIK) that the Lean kernel has a lot of fancy features that aren't yet perfectly understood from a type-theoretic perspective (I don't think Lean is unique in this regard; pretty sure Rocq and Agda are in a similar situation). And so when the kernel implements some feature whose soundness isn't guaranteed, the independent verification tools (or at least some of them) follow suit, and now any issues in the former affect the latter as well.
[0] See e.g. https://x.com/gro_tsen/status/2082483878480977959 for more detail
Huh. Thanks for bringing that into my attention, and the link!
Yes, in hindsight it makes sense that a eager LLM would exploit bugs in the kernel itself. I have not read the details yet (but want to!) and assume that it is rather related to the layers directly before or after the type-theory core; i.e. that the AI managed to get a correct typecheck by sidestepping a check during in one of the translation steps somehow, by manipulating the kernels result or by going totally hacker mode and swap implementation/overwrite memory; that is just speculation on my part though, I mainly base if on what I know about Haskell and the https://en.wikipedia.org/wiki/Calculus_of_constructions in general that have not that many constructs, and I would assume the variants used in Rocq and Lean are proven sound.
For experimental features where soundness is not proven, all bets are off IMO, but of course, that does not stop bad actors from engagement knowlingly abusing unsoundness for their own gain. Fortunately, that kind of manipulation is easy to verify when one has access to the codebase; I am would assume that something like lints for experimental features exist, or better even, something like a "sound mode". That does not help against hacking the kernel machinery though.
Concluding notes: - In this particular instance, the Collatz conjecture was appearently chosen on purpose to demonstrate the Kernel bug, from the same thread: "Not that this changes any of the above, but I am informed that the person posting the proof was actually aware that this was a Lean kernel soundness bug, and it was not intended to be taken seriously as a solution to Collatz's problem." - IF the code is made public (and it would be highly suspicious if parts of a proof where hidden), then I would assume this kind of hack is 1) easier to spot that other kinds of hack, since the asset-under-attack is really small and 2) there is not so much incentive to use much time/ingenuity/tokens on finding those hacks (the more are found and fixed, the better of course) 3) and they should be easy to defend against, I would assume; my first thought would be the flag I mentioned above that simply forbids all non-sound features, at the cost of limiting expressive power.
----
Edit: I checked, and I think it alleviates my worries in the sense that the bug(s) where not in the type theory or its implementation, but rather the machinery around it. Further context below:
That is the incident description (also linked in the x thread you linked, for future readers: https://infosec.exchange/@0xabad1dea/117002106099986943).
The following is from that thread or links from it:
- "Fixes two things: (1) more strict/nuanced handling for structure/proj interactions, and (2) adds methods for enforcing that generated auxiliary data for inductives, constructors, and recursors are more strictly checked against the assertions in the export file." | That is the fix to the non-Lean-kernel that was mentioned. To me, (2) looks firmly like what I meant with "supporting machinery", regarding (1), I do not know enough to have an opinion about it (i.e. how on what layer those interactions happen(ed)) | https://github.com/ammkrn/nanoda_lib/pull/22
- "For example, pipeline wedges (execute this instruction and the core freezes and never executes another instruction) would not be found by these techniques..." | Power and limits of Lean | https://infosec.exchange/@david_chisnall/117003914014196496
- "@mario @shelldozer it very well may be the most formally correct piece of software we've ever produced, but keep in mind it still has to run on a physical computer it's sharing with less-verified software and is also vulnerable to things like Rowhammer-class ram corruption attacks if one wants to intentionally manipulate it. There's no final escape hatch beyond which a computer can be absolutely guaranteed to always compute the correct answer, especially when someone has a vested interest in getting it to output the wrong answer." | Computer-checked proofs run on computers, which brings its own attack vectors, independent of how well the kernel is written | https://infosec.exchange/@0xabad1dea/117002712346315184
personal, cautios takeaway after reading the details: If you use Lean4 to write proofs, or read that a reputable group of mathematicians publizised a Lean4 proof, you are still highly unlikely to be fooled by a bug, and if Fable 5 decides to exploit a 0day in the core Lean4 machinery, that should still be able to be caught quickly.