AxiomProver solves an open problem

Stream: Machine Learning for Theorem Proving

[Anh Nguyễn]

There are new posts about AxiomProver proved a new open problem. Is that open problem really a big deal and is the proof of it special

[David Michael Roberts]

I guess this? https://arxiv.org/abs/2602.03722

But there are four papers mentioning AxiomProver: https://arxiv.org/search/?query=AxiomProver&searchtype=all&source=header and how Lean+mathlib are used to formalise the results

[Thomas Browning]

Maybe you're talking about this announcement: https://x.com/axiommathai/status/2019449659807219884

I think it's slightly overhyped. I don't know who Fel is, but "Fel's conjecture" is just a conjecture in this recent paper: https://arxiv.org/pdf/2012.13357. The paper has been cited 6 times: 5 times by single-author papers of Fel, and once by Axiom: https://scholar.google.com/scholar?oi=bibs&hl=en&cites=9034589070814003170

So while it's interesting to see AI start to tackle published conjectures, to call it a big deal is still a bit of a stretch, I think.

[Anh Nguyễn]

Yes, I want to mention the Fal’s one

[Anh Nguyễn]

Is it much harder than previously solved Erdos and Putnam

[Bryan Wang]

Thomas Browning said:

Maybe you're talking about this announcement: https://x.com/axiommathai/status/2019449659807219884

Genuine question here: what is "theory-building math"? (I don't know anything about the maths in "Fel's conjecture", so this is also partially a maths question.)

[Timothy Chow]

Thomas Browning said:

Genuine question here: what is "theory-building math"?

Probably they're making the same distinction that Timothy Gowers made in his essay on the two cultures of mathematics, between problem solvers and theory builders. (Gowers was of course not the first person to make this distinction; for example, Gian-Carlo Rota discussed the same topic in Indiscrete Thoughts. Interestingly, Gowers thought that problem solvers didn't get enough respect, while Rota thought that theory builders didn't get enough respect.)

Axiom Math is probably trying to say that Erdős problems can be categorized as "problem-solving math" and want to distinguish Fel's conjecture as being a different type of open problem. In my opinion, though, there's no sharp distinction between "problem-solving math" and "theory-building math." Admittedly, I'd consider it highly significant if an AI could, for example, come up with a revolutionary new mathematical concept that rewrites the foundations of a subject, the way (for example) Grothendieck revolutionized algebraic geometry with the notion of a scheme (and related ideas). That would definitely be "theory building" and not "problem solving." But the way the Axiom Math announcement is phrased makes it sound like the mathematics subject classification number of a conjecture automatically dictates whether its solution constitutes "problem solving" or "theory building," and I don't think that's right. There may indeed be something qualitatively different about this latest result, but if there is, I don't think it's best characterized using the word "theory-building."

[Bryan Wang]

I really like this paragraph in Gowers' essay and I think it's especially relevant with these recent developments in AI:

[Atiyah] makes the point (see for example [A2]) that so much mathematics is produced that it is not possible for all of it to be remembered. The processes of abstraction and generalization are therefore very important as a means of making sense of the huge mass of raw data (that is, proofs of individual theorems) and enabling at least some of it to be passed on. The results that will last are the ones that can be organized coherently and explained economically to future generations of mathematicians. Of course, some results will be remembered because they solve very famous problems, but even these, if they do not fit into an organizing framework, are unlikely to be studied in detail by more than a handful of mathematicians.

[Timothy Chow]

Anh Nguyễn said:

Is it much harder than previously solved Erdos and Putnam

It's usually very difficult to judge how hard a problem is until a large number of people have attempted to solve it. There are innumerable cases of problems that initially looked easy but turned out to be hard. Less commonly, but still not that rare, a problem may resist solution by many people but then turn out to have a short and simple solution. I find the latter case interesting, because there is a natural human tendency to declare a problem "not hard" as soon as a short and simple solution is found (the egg of Columbus effect) no matter how long it took for the solution to be found and no matter how many minds it defeated along the way. I don't agree with this attitude, and I think that the hardness of a problem should not be judged solely on the length of the solution; the psychological difficulty of solving it should also be taken into account.

There will be egg-of-Columbus people who will automatically declare that Fel's conjecture can't be hard because it has a short solution. As I said, I don't think that this conclusion is automatic. At the same time, it's not clear that anyone other than Fel worked on it before Axiom Math solved it. So I would say that we simply don't have enough evidence one way or the other that Fel's conjecture is hard (or easy).

In Axiom Math's defense, what might be true is that the solution to Fel's conjecture required the fluent manipulation of a broader and deeper range of concepts and previously proven results than was the case for the Erdős problems. I don't know if this is true, and even if it is, I again don't think this automatically means that the conjecture was "harder" than the Erdős problems. (For comparison, imagine proving a result about finite simple groups by a straightforward case-by-case verification, using the classification. I would be inclined to call the proof of such a corollary "easy" even if there is no other known proof.) But if something like this is true, then it could be an indication that AI theorem proving capabilities have scaled up by a notch, at least by some measure.

[Timothy Chow]

Elsewhere, I half-jokingly cited MacGyver and the Borg as two very different metaphors for doing mathematics. MacGyver solves problems using great ingenuity, using whatever tools are at hand, even if they are very primitive. The Borg assimilates everything that can be assimilated. So what makes a problem hard? Is it that it requires incredible ingenuity? Or is it that there is no realistic way to solve it without standing on the shoulders of giants? It sounds to me that Axiom Math's claim is more in the direction of the Borg than in the direction of MacGyver.

[Adam Topaz]

Edit: deleted since this was from the wrong repo.

[Bryan Wang]

ooh, how about #min_imports?

[Adam Topaz]

import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.Data.Nat.ModEq

Edit: this is from the wrong repo.

[Adam Topaz]

My general impression is that this (i.e. what was formalized in solution.lean) is very very very far from being "theory building" mathematics. I guess what they mean is that Fel is doing theory building.

[Anh Nguyễn]

Timothy Chow said:

Anh Nguyễn said:

Is it much harder than previously solved Erdos and Putnam

It's usually very difficult to judge how hard a problem is until a large number of people have attempted to solve it. There are innumerable cases of problems that initially looked easy but turned out to be hard. Less commonly, but still not that rare, a problem may resist solution by many people but then turn out to have a short and simple solution. I find the latter case interesting, because there is a natural human tendency to declare a problem "not hard" as soon as a short and simple solution is found (the egg of Columbus effect) no matter how long it took for the solution to be found and no matter how many minds it defeated along the way. I don't agree with this attitude, and I think that the hardness of a problem should not be judged solely on the length of the solution; the psychological difficulty of solving it should also be taken into account.

There will be egg-of-Columbus people who will automatically declare that Fel's conjecture can't be hard because it has a short solution. As I said, I don't think that this conclusion is automatic. At the same time, it's not clear that anyone other than Fel worked on it before Axiom Math solved it. So I would say that we simply don't have enough evidence one way or the other that Fel's conjecture is hard (or easy).

In Axiom Math's defense, what might be true is that the solution to Fel's conjecture required the fluent manipulation of a broader and deeper range of concepts and previously proven results than was the case for the Erdős problems. I don't know if this is true, and even if it is, I again don't think this automatically means that the conjecture was "harder" than the Erdős problems. (For comparison, imagine proving a result about finite simple groups by a straightforward case-by-case verification, using the classification. I would be inclined to call the proof of such a corollary "easy" even if there is no other known proof.) But if something like this is true, then it could be an indication that AI theorem proving capabilities have scaled up by a notch, at least by some measure.

Yes, it is surely true that the length of the solution does not reflect the difficulty of the problem

[Anh Nguyễn]

Conway’s knot is a problem that stood for a long time but then solved

[Anh Nguyễn]

Its solution is not too long

[Kevin Buzzard]

One observation that can be made for all of these "open problem was solved by AI and the solution turned out to be short" problems: whether or not you want to conclude that the problem was "in retrospect easy", you have to concede that (a) the problem was solved by a machine with no human involvement and (b) that humanity didn't seem to know the answer before, but now it does. This in itself is intrinsically interesting whatever the "easiness" of the mathematics.

I think my reaction to anyone who looks at the shortness of the proof and, without reading it, deduces that Fel's conjecture was "easy" would be to simply challenge them to prove it without looking at the published proof, because for sure the statement is very easy to understand.

[Adam Topaz]

i completely agree. What I disagree with is the "theory building" claim.

[Michael Stoll]

Adam Topaz said:

import Mathlib.Algebra.Order.Ring.Star
import Mathlib.Analysis.Normed.Ring.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.Data.Nat.ModEq

I'd hazard a guess that the two .Star modules are not really necessary.

[Adam Topaz]

give me 10 mins and ill tell you exactly what the proof uses from those modules

[Aaron Liu]

probably typeclass instances which could also be inferred a different way if you remove those imports

[Adam Topaz]

yeah, you're right Aaron. Those two imports are redundant.

[Adam Topaz]

The other two are not.

[Adam Topaz]

I got the import set down to the following:

import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.Order.Ring.Int
import Mathlib.Data.Nat.ModEq
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Zify

[Kevin Buzzard]

Adam Topaz said:

i completely agree. What I disagree with is the "theory building" claim.

Yes. Surely AxiomProver solved a problem here so that Fel could build a theory.

[Adam Topaz]

Wait, the arxiv link mentioned above doesn't seem to be the correct one (the code I was testing was from the git repo mentioned in that paper, but it seems that the solution to the conjecture is here: https://github.com/AxiomMath/fel-polynomial )

[Adam Topaz]

This is less elementary as it uses Mathlib.NumberTheory.Bernoulli

[Bryan Wang]

I think

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Data.Int.Order.Units
import Mathlib.NumberTheory.Bernoulli
import Mathlib.Tactic.IntervalCases

works

[Adam Topaz]

Yeah, I got it down to exactly that import set as well.

[Adam Topaz]

I must admit, I do find this proof to be pretty impressive to have been done by AI.