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 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.
> 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 domain more suited to mathematical proofs that can be formalized using Lean4, when it comes to using LLMs. The fact the hype-circle started earlier in software than in maths is due to the difference in monetary incentives. (Or another, rather and not really serious radical 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 lickely to be correct)
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
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.
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.
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.)
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.
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 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.
> 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 domain more suited to mathematical proofs that can be formalized using Lean4, when it comes to using LLMs. The fact the hype-circle started earlier in software than in maths is due to the difference in monetary incentives. (Or another, rather and not really serious radical 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 lickely to be correct)
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
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.
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 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?
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.
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
I thought SAT like the high school admissions test