AI in mathematics is forcing big questions
spectrum.ieee.org
spectrum.ieee.org
> A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs and abstractions, without which no autoformalization could take place. By contrast, Math Inc’s autoformalized proof of Viazovska’s results exposes no intelligible interface. Who in their right mind would merge a 200,000-line unaudited vibe-coded blob into the master branch of global human science?
https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...
If there are other lemmas, etc buried inside that 200k blob that can be factored out and proved and used themselves, so much the better. But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me. I see no reason not to accept the vibe coded blob if Lean says it's kosher except anthropocentrism.
(i) accepting that a piece of code is a valid Lean proof (ii) merging a valid Lean proof into Mathlib.
Valid Lean proofs need maintenance. Mathlib is a living blob of code. People care about how fast the proofs typecheck. Many other properties of code play a role.
Not everything that is true is worthy of immediately including in the Encyclopaedia Brittanica.
As far as I can tell from colleagues in other domains, it’s the same there. One paper will mention something off-hand and that’ll cause someone else to have a spark of insight, which turns into it’s own valuable research
Mathematics has to be also understood from the perspective of theory building, not just problem solving.
I couldn't disagree more.
A lot of mathematical "problems" are almost entirely pointless. Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map - it is the math that is developed during the solving process that is valuable!
An answer to a question like "what is the exact area of a unit circle" is a mere curiosity. Calculating a good-enough approximation is trivial, after all. But wanting an exact answer leads to developing calculus, which leads to most modern physics. Science was able to make a giant leap forwards due to the techniques developed, while the actual answer itself is mostly useless.
But let’s consider a hypothetical: what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind? If there truly is no way to simplify some proofs down from 200,000 line incomprehensible gibberish to something you could teach to a high schooler or undergraduate or even a PhD. Is the proof still worthless? Sure, at the moment, it might be. Finding such a proof and understanding the implications of it are different skills, the latter of which AI almost certainly does not possess at the moment. But there may come a time where the AI can view the bigger picture and make the leaps you described (say, an eka-Calculus from an eka-unit-circle). These leaps may be as unintelligible to us as the proof in OP is.
I guess the question is: assuming that we can’t make the proof beautiful enough to spark deeper human understanding, do we still want it if it sparks deeper AI understanding?
Personally I would hate to live in a universe where the boundaries of science are beyond intuitive human understanding, but I think it’s almost certainly the case. The idea that the rules are all within our grasp reeks of anthropocentrism to me. I would love for the universe to prove me wrong though. It’d be a pleasant, hilarious coincidence if they do fit within the boundaries of our understanding.
Mathematics and science are both about building structure on large classes of facts about the (logical or physical, respectively) universe that allow us to generalize our knowledge and make predictions about facts we cannot yet observe. This also lets us make claims about things that are, individually, too complex for the human mind to grasp, by abstracting away the complex details into a simpler structure and then making the claim about anything that satisfies that structure.
To put it another way, mathematics is about finding beauty — specifically those things that exhibit structure that humans can grasp. Modern mathematics, for the most part, makes no claims about what lies outside that space: if it turns out that the universe consists only of things that humans can describe through mathematics that would be neat, but in the much more likely case that it doesn't mathematics continues as it is today.
It's an interesting and maybe even useful trivium if (according to some set of axioms, such as those implemented by your favourite proof assistant) a fact is true, but it's not (human) mathematics, and if there's no useful way for humans to generalize from it there's no point in including it in a library of mathematics. It wouldn't be that surprising (but would be very interesting!) if there were an entire parallel class (or, more likely, family of classes, one for each AI architecture) of AI mathematics comprising structures that AIs can usefully generalize from. Such a thing has no reason to bear any resemblance to human mathematics, which is based on mapping structures to innate human linguistic and spatial intuitions, and may not yield any insights to human mathematicians.
By extension: why should we assume that a human would still understand the problems - or the answers? If all of it is complete gibberish to a human and can never be applied in any way, shape, or form, then what's the point?
The way I view it there are two options here: either you completely ignore it and end up burning a massive amount of electricity on what is essentially a bunch of LLMs jerking each other off, or you blindly follow it and end up with a Machine God who can justify a genocide with a "This is the correct thing to do. Trust me bro, I have irrefutable proof - you won't understand it". There's just no sensible way to do post-human math in an inherently human world.
"Okay, so what determines what is and is not allowed in the collection?"
"Whether the given substatement is true or not, of course."
Like this is obviously silly, right. In your view you could have two guys both trying to prove or disprove that the area of the unit circle is 3, and yet only the guy doing it with some vision of nobility where he's building up to this grand theory of approximations is the one actually doing "real" mathematics. The guy who's doing it just because he thinks it's neat and would like an answer to the problem itself doesn't count, and you suspect he couldn't even exist.
What did the alchemist truly learn from this interaction? Is the answer in any way helpful for him? Will it lead to him making gold, and the implied endless riches it entails? Why should it bring him him to ask follow-up questions with useful answers like "The technology to do this doesn't exist yet and can't be developed within several lifetimes" and "It'll never be economically profitable to turn lead into gold", instead of blindly being fed piecemeal steps in the impossible task of one medieval guy building a LHC?
Writing true statements is absolutely trivial, anyone can do that. There's an endless amount of true statement which have absolutely no value to humanity whatsoever. Their proof is meaningless without something to give it context. "Substatement 1304 is true" has significantly less value than "here's something I call 'group theory', and it might also be helpful solving open issues in fields X, Y, and Z".
Mathematics is about widening our collective understanding. There will of course be some people out there who'll hear "The answer to life, the universe, and everything is forty-two", think "Neato!", and go on with their day without giving it any further thought - but I'd have a hard time calling them mathematicians.
That doesn't mean it is completely useless, of course. A "prove that no efficient algorithm exists to break this new encryption scheme" would be very helpful indeed. Until you realize it neglected to take quantum computing into account, of course.
[0]: https://home.cern/alice-detects-conversion-lead-gold-lhc/
Now if you ask "does the area of unit circle equal 4?", I don't really know, but we can go back to the oracle and ask again (we haven't learned the general pattern).
Also, I'm not sure that assuming this 'area of circle' question was cutting edge math, that the oracle wouldn't say 'yes, to a certain level of tolerance'. Can't count how many times I've seen agent decide a test needs to be loosened or deleted because its an "edge case" or "blocking". If you don't understand the proof you might get back 'yes' for some versions of 'is the area of unit circle 3' (depending on complexity of that ask).
> Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map
I agree that solving problems along the way is incredibly useful too, but there's no math problem that I'm aware of that's utterly useless. Thing is, math is about abstraction and structure. You're developing tools. Those tools can be used for more than one thing. That's why math is often called a language. It's also why mathematicians and physicists end up being so helpful in other fields, because it was (most of them) about understanding the language of complex problem solving. Even code is math (I find it quite odd programmers are against math and elegance as these are directly in line with their goals, but I guess there's always a Dijkstra EWD already calling this out)
Where I fully agree with you is that solving hard problems advances us. TBH, it doesn't matter what it is. Fund NASA and you not only get men to the moon but velcro, GPS, and global wireless communication. Fund particle accelerators and you get the internet. Fund math and, like you said, you get a tool (calculus) which is worth more money than we can even imagine. The thing is that solving hard problems forces the unknown unknowns to become, at least known unknowns.
The beauty of the weapon IS the point. What it proves is derived from its use.
The laws of mathematics exist and their truths hold before they are proven by humans or our machines, so in a very real sense the entire point of proving anything in the first place is anthropocentrism.
That, plus cleaning it up may reveal it contains proofs of other things we also want to know. Imagine if this happened to also contain as a sub-part a proof of all the open Millennium Prize Problems? We don't know until we investigate. (If it was a specific list of things to check from rather than expanding humanity's library, we could just ask an AI to do it for us… but as The Wachowski sisters wrote in their most famous script: "I say your civilization because as soon as we started thinking for you, it really became our civilization").
So yeah, generated machine-valid proof can be denied if it's incomprehensible, same as human machine-valid proof can be denied for same reasons.
just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.
Exactly! There's a shared foundation, and everyone builds upon it. A mathematical paper is a whole bunch of Lego blocks being added to that foundation, and combining them in a hopefully-useful new interface.
But if the entire paper is just one giant black box, you only get to use the final interface: you lose the ability to meaningfully repurpose the individual Lego blocks to build a different interface. You end up having to reinvent the same Lego blocks over and over again, just with a slightly different color each time.
Don't want to re-prove each and every Lego brick? Then you shouldn't accept giant black box proofs.
Replacing thought and curation with repeated automation is tech debt, pushed down to fundamental knowledge and understanding.
Have I treated your argument unfairly?
Why not just fork the original master branch of human science to an ai-enhanced one and see where that brings us?
This future of "the AI built the compiler and it's totally incomprehensible spaghetti, but don't worry, it verified the compiler works using this AI-generated proof assistant whose codebase is also pure spaghetti" terrifies me.
Please show me a proof of `False` in Lean.
LLM agents will a) discover dumb counterintuitive stuff like this and b) exploit it to satisfy the kernel with c) the questionable lines being buried behind millions of lines of math slop. Humans have to check this stuff.
The idea behind the challenge to provide a few lines of human-written/checked scaffolding that defines an "API surface". The API surface is resistant to junk/slop filling out the sorry's. This is supposed to reduce the number of lines that humans have to read to only a handful, while the full valid AI-generated proof is tens of thousands of lines. The challenge was just solved a couple weeks, here's the discussion about it: https://leanprover.zulipchat.com/#narrow/channel/583336-Auto...
The novel approaches to solving challenging proofs is very useful.
Here is a other one: hello_world.c versus hello_world.exe (apologies for windows extensions, just for illustration).
One is made by a human for human consumption and extension (though legible by a machine). The source code.
One is made by a machine for a machine. Unreadable by a human. The "binary", though that's a terrible misnomer. (Sure you can disassemble but any nontrivial program is too much to cope with as a whole).
Source vs binary. Both are useful but only one is useful for human consumption.
Anyone who understands type theory and how theorem provers work? It's sort of akin to saying "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!", you know because the compilation would have failed otherwise(this is different than saying the program behaves correctly, but that's precisely the difference between formal proofs and compiled programs).
The entire argument both you and Bessis are implying is that mathematics must be human intelligible. But there's absolutely no reason to assume that every mathematical statement must have a human intelligible representation. There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use.
Just because people who don't want this to be true, and I can understand the motivation, doesn't mean that it isn't still the case.
It remains all of those things, sitting alone in its own repository of 200kLOC; what benefit comes from merging it into mathlib?
> There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use.
This is obviously silly:
Things that aren’t human intelligible aren’t human usable, so the restriction is necessary to have a collection of things humans can utilize.
This is objectively false, people use things every single day they don't understand. We still have plenty of things about the world we don't understand but still find useful.
You are saying anything we know to be the case, but cannot understand why cannot be used? Can we just stop sleeping because we haven't reasoned why sleep is necessary even though we know it is necessary? I mean we still don't really understand gravity (we know how but not why)
In the 40k universe, modern humanity is below not just their peak of technological prowess, but even their peak of pre-AI prowess. Because they landed in a valley of superstition involving machines they do not understand — and have no way to rebuild towards their peak, without yet further losses by moving away from the magical machines.
That has nothing to do with the universe at large — and everything to do with human society and choices. Which we do have control over.
The comment I replied to equivocated between absolute limits to comprehensibility to humans and sociologically constructed limits, implying that thinking there may be the former makes someone ‘fine with’ the latter. That’s nonsense.
They approximately use them with varying degrees of success, but also mistakes, broken inferences, etc.
My exact point is that your view reduces our ability to do mathematics to that broken, flawed usage and thereby undermines its utility for logical precision: mathematics is only useful because we cleanly understand it.
When you try to use mathematics without understanding, you cause disasters: stock market crashes from mispricing options, Amazon’s 2018 hiring freeze from misallocating $1B, etc.
Note: neither of your examples (sleep, gravity) are things that people intentionally use. They just happen to people.
I think it’s very telling you couldn’t think of an example.
So what will you do if the doctor prescribes you an LLM-vibecoded drug that nobody understands how it works, yet it cures some deadly affliction with close to 100% efficacy?
What if, say, these incomprehensible math results lead to a revolution in quantum physics which unlocks chip topologies that are orders of magnitude faster than human comprehensible designs?
Would the high priestess of human reason pass her divining rod over such chips or life-saving drugs and reject it as the work of the AI devil?
Again, my exact point is that mathematics loses its utility when you reduce it to that inaccurate usage. You no longer can have any faith in the conclusions — just like sometimes psychiatrists kill their patients with an SSRI prescription because they don’t understand the drugs.
> Would the high priestess of human reason pass her divining rod over such chips or life-saving drugs and reject it as the work of the AI devil?
My point is you can’t know if you’re turning it over for life saving drugs or poison, if you don’t understand what you’re getting.
If you give me an inference chip that runs 200x faster, yes, it could be backdoored to take control of my dishwasher and kill me in my sleep - but I can't deny it runs 200x faster an account of nobody being able to explain why. The same for the mistery cancer drug that cured everyone who took it up to now, but could, without doubt, kill the next patient.
The telco that manages loads and allocates networks knows how voice compression works.
The farmers and supermarkets know how the supply chain works.
None of your questions show why mathematics should include blobs of incomprehensible gloop, where no mathematician, no logician, no philosopher, no man on the street can make sense of said gloop, or use it in any way to further human knowledge.
When it's been decomposed down we can discuss this further, but now it's like saying red is red, just because.
But I'll take your expanded statement, to include riding a horse, something even older than the engine. We don't understand fully how a horse works -- biology is still a matter of seeing fragments of the whole -- but people had no problem riding and breeding them before the invention of the car, and before the discovery of genetics.
Meanwhile, understanding the math of a thing -- like stock markets, or nuclear bombs -- does not prevent its use from going badly.
Math is useful and beautiful, and a helpful tool for expanding our understanding of the world, but it is not the whole of understanding, or the sole factor in successful application of science to the world .
Signed, a mathematician.
I think it might be fair to say that a proof cannot be without value if it proves something meaningful to a human, that a human can use somehow? But such proof probably doesn’t belong in a library seemingly explicitly dedicated to human-graspable proofs. Just because it violates the intent.
It’s not like such proofs mustn’t exist at all.
If you go to the fiction side of things, you’ll get a lot of things that humans would like to do, but can’t right now as we’re blocked by physics laws and our own biology. We have harnessed electricity, why can’t we harness gravity?
Reasoning by analogy...
Would we still be able to use computers? Of course! They don't need the source code to run.
Would we nevertheless be in big trouble? Oh definitely. We'd need to write all software again, from scratch. Some critical parts we could reverse engineer. Maybe even derive some structures that translate back into source code, but only because a human wrote that source code in the first place.
Hopefully the point is clear: A proof, even if it is correct, that is totally obscure and unintelligable by humans is not very useful for mathematics. It's a black box that doesn't further understanding of the structures and approaches to think about them, and that's what math is all about.Just having a big binary blob of a program doesn't help much if you want to add a feature.
That's also why biology is so hard. There is no source code. It's just millions and millions of years of evolution and things have evolved in weird ways that don't really make it easy to understand them, even though they clearly work.
I'll remind you of the underhanded C contest and the fact that LLMs are widely documented to take such routes.
Yet they don't merge this stuff, for many different reasons, including that those 200K lines are free as in puppies.
You can have all the type theory of the world, but the library still needs maintenance.
Change a simp-lemma in a file close to the root. Oooh noes, now there's 987 errors in the 200K loc that we merged last week. And there's nobody there who understands how to fix them.
Just use AI to fix. Or maybe just don't merge the code and let it sit in a downstream library?
And wait until there's evidence that the code is stable, high-quality, with well-designed APIs. And then decide that it might be worthy including in a more foundational library.
So why don;t they use AI to write Lean programs? That should make the AI-proofs more readily human undersrndable.
> In particular, the process of converting a medium-sized Lean document (containing a few thousand lines of code, with some proofs AI-generated) into a nicely golfed and structured Mathlib submission has been an interesting experience. AI agents can be used to perform local golfs that can shave the size of the code somewhat, but global refactoring decisions, such as noticing that a certain argument appears multiple times across the document and can be abstracted into a standalone lemma that can may have additional utility beyond the file, is still largely beyond the reach of current AI tools. (I find that I can explain such a refactor to an AI agent, who can then execute it, but they struggle to spontaneously discover such refactors on their own.)
Of course there's no reason AI couldn't do that too.
When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it.
In those cases, we usually write tests.
But when tests get too big, we end up writing tests for the tests.
Eventually, it feels like we're heading into an era of proofs for proofs.
For me, this problem usually unfolds like this:
1.I can't trust SDKs or Stack Overflow code.
2.So I write tests.
3.But I can't trust the tests either.
4.So I use test coverage, mutation testing, property testing, and fuzzing.
5.If that's still not enough, I add formal verification.
6.And then the problem becomes: can I trust the verifier?
That's how it ends up. Wouldn't human work shift toward verifying the verification systems themselves?
What does that even mean? Sorry, this is just a nonsensical term.
The issue is not that the proofs could be wrong. It's that humans don't understand them even if they are verifibly correct.
In contrast, with software you don't know if it's correct. That's what you have a test for. Even if you understand it, there could be a bug. And tests could have bugs too, so you can have tests for tests. But proofs that are verified are correct. That's it.
Imagine you have a program that is formally proved to be correct. You don't need a test for it. However you might not understand it. Having a test or not does not change that.
TL;DR: Correctness and understandability are (mostly) independent properties.
One thing I might add is that not all programs can be proved to be correct for the simple reason that not all purposes of a program can be mathematically specified. For example, for (even "closed world" domain programs like) a chess engine, the one thing that matters (in the absence of a complete solution of a game like there exists in checkers) is "can beat world champions", which can only be tested empirically. Or sometimes, e.g. business logic software, the purpose can be mathematically specified but not in a simpler way than the code itself.
Also code is a mathematical object, but running code (the process) is not because it’s just electricity in metals and semiconductors. We modify the voltage somewhere and that leads to a transformation (light in displays, sound in speakers,..) somewhere else. We do have models for all of this but they are approximations, not the real representation.
There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understanding. I like this one quote by (allegedly) Wigner that illustrates it well:
"It is nice to know that the computer understands the problem, but I would like to understand the problem, too."
But a montage about weight lifting does not a body builder make.
But why should it be the case that this is always possible?
It's entirely reasonable that the set of useful mathematical proofs is a proper superset of human intelligible useful proofs.
In fact, to argue the contrary would imply there is something incredibly remarkable about human cognition.
Just that the set of proofs a human can interpret and the set of statements a human can understand overlap; conversely, you require that the statements/theorems humans can understand be a larger class than the proofs they can understand.
To me, it’s not obvious which of those should be true:
- can we only understand theorems for which we comprehend their proof?
- or can we understand theorems despite not comprehending the proof structure?
Within the mathematics community, opinions differ. But you’re elevating your perspective on that question into a law, without any evidence.
I don't know what your distinction between "understand" and "comprehend" but my point was not about these words, but about being "useful" and being "understandable".
I'm saying there's no relationship between a mathematical statement being useful and it being understandable.
If it is true that "understanding is a prerequisite for usefulness" (where "understanding" means that a statement can be proven in a way that is intelligible to humans) was a property of mathematical expressions, then this fact would certainly be useful (we could exclude any statements that no human understand from the world of useful mathematical expression). But, by that definition, we would need to understand that statement, so you would need to be able to prove that "understanding is a prerequisite for usefulness" in a human intelligible way.
Now what I just wrote is in itself not a proof that we can't know, but proving the above statement would involve expressing the claim in a mathematically verifiable way that was also understandable by humans, which does imply something remarkable about human cognition (something that would be intelligible no less!)
You're acting as if current-day AI comes even remotely close of surpassing it, lol.
In fact, please show me a useful mathematical proof unintelligible to a human, or even if you would like to "assume" the existence of such, explain how it could be useful to anyone.
If you can't explain something in a way that a child could understands it, you don't fully understand it either.
I don’t see that LLMs will fundamentally change this, but rather accelerate the speed of mathematical research.
Some computer generated proofs might of course be hard to understand, but at least their existence gives another data point work with.
Doing Mathematics is more than proving something, that’s just the end of a long road spent pondering at one’s desk about how things could work out.
> “Programming is understanding. If you don't understand what you are doing, you are not programming. You are generating text.”
Perhaps a proof without understanding is just generating numbers.
in medicine they use all kinds of drugs which they don't really understand how they work. anesthetics is a great example
Now they have a valid excuse that the human body is incredibly complex and not yet understood. We don’t have that excuse, because we build all of our software from the ground up. If we don’t understand it, that is our fault.
If you don’t understand the problem you can’t be sure that the computer does.
A fundamental property of any formal proof is that it can be checked by a fairly stupid machine, automatically, because every step is a simple mechanical operation that names one of a handful of axioms and refers to a handful of earlier steps, the truth of which has already been established. So while coming up with a proof may require genius-level thinking, checking an existing fully fleshed out proof is simple -- just potentially very tedious because of the sheer number of steps.
That said, a typical human-written proof omits many steps considered "obvious" to a trained mathematician. Converting this to a formal proof involves interpreting what the original author "must have meant", which requires a lot of expertise and can go wrong -- or it may reveal that there is some inconsistency in the original claim itself.
The controversy around Mochizuki and the "abc Conjecture" proof is a contrary example.
Last time I checked, it was a disagreement over whether an informal proof is sound, which is exactly the problem with informal proofs.
ETA: There might be a misunderstanding about what "formal proof" means. Even a very detailed, precise English-language description of a proof is generally not a formal proof. The bar is essentially: "It could be checked by a machine that follows simple rules." If different interpretations of a "proof" are possible, the "proof" is by definition informal. Informal proofs are valuable because they are strong evidence that there's a corresponding formal proof "underneath" that would establish the theorem's truth, and because they are (usually) much easier to understand.
This is one of the great things about formalization: it would have avoided this entire debacle.
It's also a MASSIVE amount of SUPER TEDIOUS work. And it's the kind of work that folks who think up advanced math proofs tend to loathe. It's along the lines of programming by toggling in the code from front panel switches.
So what current mathematics does is judge a proof by whether or not the application of the proof somehow coincides with the result from some other adjacent branch of mathematical knowledge. So, a "novel" proof is expected to either help prove something in a slightly different branch of mathematics or simplify some already existing proof.
And that is, as I understand it, the crux of the matter with the Mochizuki proof of the "abc Conjecture." Solving the "abc Conjecture" should provide tools for solving other similar problems just like Wiles' proof of Fermat's Last Theorem provided an entire class of tools for dealing with modularity and elliptic curves. And yet Mochizuki seems to unable to do or demonstrate any of that.
So, Mochizuki's work is like someone dropping a gigantic and impenetrable proof of exactly and only Fermat's Last Theorem that doesn't apply to anything else. Sure, it would be an interesting (and true!) thing, but without the ability to use it further, it's a curiosity rather than a pillar.
It was, but now autoformalization is a thing. If he had delivered his proof and a formalization -- no matter how much it looked like autogenerated slop -- he would have been taken much more seriously.
Despite reluctance to do formalization, I expect it will gradually become required to get math published, since journals will be flooded with AI generated slop. It will be necessary to filter the slop, and requirement of formalization in the supplementary material would be a good way to do that. It would still be necessary to check that the formalization of the statement of the theorem is correct, but that's a much smaller ask.
But I also definitely don't understand the problem if I can't get the computer to understand it, with tests.
In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.
With all of these questions in the air, epistemology might be making a comeback.
I disagree, software engineering is a mature discipline now, and at this point we have so many testing frameworks (unit testing, syntax testing, regression testing, fuzzing, testing end to end, live, with a subset of known good and incorrect inputs, chaos monkeys, etc, etc, that to say "there's no way of verifying the AI-generated code" is frankly incorrect.
Or, if you insist, defend the "there's no way of verifying the code, at all", and not only AI-generated.
(if it helps I work in the company where before the code even starts being written, several extensive tests for it must be ready first. It's hard to even commit a broken code, and later in the pipeline it's very easy to catch the subtly broken or incorrect code)
> In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.
Type theory can also be an independent synthetic foundation atop which you build mathematics.
Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.
No.
In particular, until now, mathematics were one of the rare sciences were great scientists could emerge from any country with a good education system.
With the raise of strong AI tools, only scientists in rich countries with access to those tools might be able to advance faster on the most difficult problems like the millennium problems.
Mathematics might become like experimental sciences were you need to build expensive machines to make further progress, such as nuclear fusion.
Actually, even now, the strongest models in mathematics are only available to a few engineers and a few mathematicians selected by Openai and Google.
But would they be able to realize their potential without further (mostly monetary and institutional) support from their country? In that way, things now are not so different from before. However, the story will probably change in a few years' time.
Computational intelligence obviates the role of the human in making capital reproduce and multiply. Mathematics as its own field of study might become pointless other than as a hobby - an endeavour reserved for those entitled to the machine's output. What the machine develops in the place of mathematics may not be recognizable enough to even share the same label - that is, if it even uses mathematical principles rather than just finding correlations that are 'good enough' for its use.
Would some one with tokens to burn mind checking that statement out and post back. Be sure to use long dashes too.
i.e. You have to be a good engineer to understand the well generated LLM code and a program
Meanwhile, if you put honorable people in charge and trust them to do the right thing, they can figure things out ad hoc.
Unfortunately, mathematics suffers as a bystander. But the good news is that the muggles will always want to keep the eggheads around because they would rather die than think about the negative consequences of having their dreams come true exactly like they wanted.
Priests were interpreting the oracles (at least at a place like Delphi) according to the context of the people asking the questions aka participating in politics of that ancient times.
Subjectivity was a feature and I’m not sure that fits to mathematics though.
I wonder if mathematics as a science field moves more into engineering or if a different branch will emerge that is closer to that because to the point of the article, science is about understanding not just results.
This is a decidedly anti-enlightenment statement.
However given the history of mathematics that's not really out of order. There's a lot of mysticism intertwined with early mathematics and it's only relatively recently that mathematics has taken the beads out of her hair, put on a business suit, and gotten to work.
I mean even Galileo's, the patron saint of skepticism, job was observing the stars so that he could write horoscopes.
And we see the attitude repeated even today. I work in a technical field and whenever I mention that I think type theory is kind of cool the response more often then not is for them to give me the ol' "Thank goodness for people like you, I'm just not a math person."
If mathematics is human understanding of logical consequences, understanding is the priority. But if AI proves something we can't understand but can utilize, that is a different sort of useful.
We are getting awfully close to "the answer of the universe is 42" and having it not be a joke...
I couldn’t build an internal combustion engine or even a plastic box, so maybe there’s nothing wrong with this approach.
> Some worry about the accessibility of AI tools. Traditionally, mathematicians have required little more than intuition, training, and a pen and paper to advance their field. If this slow, deliberative process is no longer valued by society, and particularly by research funders, then mathematics could become an elitist activity, only practiced by select organizations that can afford to work with proprietary AI models.
This can be true of anything LLMs do better than existing options. Because the best LLMs require enormous resources to develop, access to them can be very limited. Right now they are priced for market share. What happens when your small law firm attorney, or self-representation, goes up against a large firm with LLM expertise? Can the kid from the poor high school compete with the kid from the rich school with premium LLM access, in mathematics for example?
the poor kid always had disadvantages, had to help the family, while the rich kid could focus on the math, and maybe get into a good math place with family help
So much that has been true for millenia we've changed in the last century or three.
You aren't having the AI check the proof, you interactively work on the same LEAN proof, handing off between the AI assistant and having LEAN check it and provide feedback for both of you when there's a mistake.
It can definitely be a good research assistant though
I had assumed that the recent OpenAI solution to an Erdos problem represented original mathematical thought.
I went looking for more details, and found this Scientific American article which provided some nuance I had previously missed, namely that the mathematicians involved don't think genAI created any really new mathematics - just applied what existed in an intelligent, elegant way:
So, impressive though the result is, perhaps your claim has more grounds than I had thought.
(edit: lol didn't realize the sibling comment below is essentially my comment)
If it's utility, then why doesn't AI deliver utility? Isn't this an argument for AI?
One can expand this to various kinds of utility. Is knowing mathematical statements are true useful? In the ability to produce proofs useful? Does being able to prove carry over to other kinds of reasoning? Is producing a cadre of math-capable people useful in wartime? Is national prestige of value? There's a pro-AI reading of all these.
It it's beauty not utility, then why isn't math funding over with art funding, along with hills covered with acres of fabric, motorized embalmed animal carcasses, and religious symbols in bottles of urine?
The entire field of cryptography is built up on number theory, a field which famously a major contributor chose because it could never be useful [for war].
It is precisely NOT about big questions but rather potentially covering and thus cornering away all the "small" questions.
PS: already argued for something similar in recent Ergos related work, see comment history.
I've been in the software industry for 30 years and I understand that sentiment perfectly on a personal level. However, also having used ChatGPT for the first time this year to help solve a technical problem, I was surprised to learn that feeling didn't go away. In fact, it was because I leaned on my experience and technical understanding to get to the point where I realized I needed help that I decided to try a new tool. I didn't feel any shame or disappointment in myself, rather I felt excited to learn something new that came out of the solution. It sent me on a new path of learning.
Now, that was research and not implementation. While plenty of code options were presented by ChatGPT, I analyzed the solution and educated myself from it. My final fix looked very different from the proposal because I do things a certain way, based on experience and learning from my many mistakes. In this scenario I was the secondary verification. My peers the tertiary. AI made the proposal, humans did the verification and could not have done so without cumulative knowledge and experience.
I have to assume that all fields utilizing AI will remain as they have always been, human education and experience will come first no matter what the tools available, because we are the ones impacted by the data produced by AI. As many math-oriented commenters here have already noted, human verification is a necessity and to do that, you must understand the discipline within which the data is being produced.
Personally, the idea of reaching solutions in math and computing (for example) exponentially beyond human capacity is exciting; I want certain answers before I die! But it still must be human-verified and the solutions should be for humans, not for machines, and not for "time to market". Repositories full of unvetted AI-generated code is bad enough, but once you start engineering structures, spacecraft and medicine strictly with AI, well...
It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify the correctness. One hallucination in 300 steps of logic is enough to destroy the entire proof.
If you have the LLM generate Lean code, and it compiles, then the proof is correct and you don't need to bother checking its working. (You still need to check that it is proving the theorem you asked it to prove).
But let's assume Lean is perfect: - you have to trust your file system - you have to trust your OS - are you sure your monitor displays "proof is valid" correctly - maybe there's a bug in your CPU hardware? - or background radiation flipped a bit in your RAM - do you trust your brain? Maybe you went to bed last night firmly believing "that proof is wrong" and you woke up this morning with a different belief that "the proof is valid".
It would be interesting to see how Lean is being tested. Pummeling it with inputs from AI proof search engines sounds like a good way to expose hidden bugs, just as pummeling a compiler with randomly generated programs is a good way to expose previously unknown compiler bugs.
It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean.
> One hallucination in 300 steps of logic is enough to destroy the entire proof.
The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired.
In fact, it was Wiles himself who realized there was an error.
> After the announcement, Nick Katz was appointed as one of the referees to review Wiles's manuscript. In the course of his review, he asked Wiles a series of clarifying questions that led Wiles to recognise that the proof contained a gap.
It seems likely Katz played a crucial role here.
Wiles is just a prominent example. In practice, other humans often play this "verification role" for mathematicians, whether via a formal review process or informal discussion.
I hope mathematicians have the self-respect of not establishing rules such as "if a proof is longer than X, break it up in smaller ones, otherwise it'll be outright rejected".
Yes the "truth" (doesn't exist, see Gödels theorem) is discovered in a vast, wild landscape that Mathematicians explore.
But which areas are worth exploring is a critical question. Partly driven by application, partly aesthetic. It's a quest for simple things that are a bit surprising, or that were hard to make the statements so simple.
People get confused by this created/discovered thing. Of course it is discovered. It was there even before you created it. ;-)
The quality of the mathematics is a function of who has authored it?
Is direct experience and struggle really the only driver for developing intuition?
This is not the "standard" advice that usually gets peddled but for me it "worked".
As an aspiring amateur of recreational mathematics, it gives me joy to find this recommendation and start reading the series. It reminds me of Martin Gardner's "Mathematical Games" column, and its successor, Douglas Hofstadter's "Metamagical Themas".
For a while now I've been chewing on Baez's paper, "Physics, Topology, Logic and Computation: A Rosetta Stone". I'm intrigued by it. At first baffled, then continued studying related topics, coming back to re-read and appreciate what it's saying. I'm exploring what it means from the computation angle, in the context of Haskell Curry, combinators, lambda calculus, cellular automata, rewriting systems. And more far-fetched thoughts, like Stephen Wolfram, Max Tegmark, or how it may relate to biology such as Michael Levin's research.
On the role of AI in mathematics, it brings up more questions about the use of computers in experimental/exploratory mathematics. Part of the concensus emerging, it seems, is the formalization of programs as proofs, in particular the Lean language ecosystem. It's like the field of software engineering is rediscovering its roots.
The deeper I go the more I want to participate, write and talk about the fun things I'm discovering. Maybe one day write a paper of my own, if I can manage to do it in a respectable rigorous manner. For that I know I still have a lot of basics to learn, cultural etiquette too, and probably lean on something like Lean to be able to demonstrate that the ideas are sound.
>> In February, for example, the AI company Math, Inc. used its aspirationally named reasoning agent Gauss to formalize a proof that had earned the mathematician Maryna Viazovska, of EPFL, in Switzerland, a Fields Medal in 2022. Gauss first helped human mathematicians complete the formalization of Viazovska’s solution to the 8-dimensional sphere-packing problem in a matter of days, and then autonomously formalized the more complicated 24-dimensional case in just two weeks.
Gauss "autonomously" formalized? There are no autonomous AI systems! Even the most performant agentic harnesses require extensive human guidance and cannot complete substantial problems without some user interaction. Indeed, if I read the Math, Inc. pages linked in the article I find that Gauss is a typical agentic harness that relies on human scaffolding and interaction and its vaunted autonomy is currently only speculative:
>> Gauss offers a glimpse of how formalization will scale into the future. Currently, it relies on natural language scaffolding supplied by human mathematicians, and requires high-level expert guidance and development on that scaffolding. We anticipate future iterations of Gauss to be more capable and autonomous.
Or take this bit from the Math, Inc. pages again:
>> In two weeks, Gauss then autoformalized the 24-dimensional case using only the original paper as input, performing autonomous literature searches when needed. This brought the total sphere packing formalization from 70k to ~200k lines.
https://www.math.inc/sphere-packing
Gauss took only the original paper as input? Really? No initial prompts? No scaffolding? Just the paper and off it went? But then, the future feared by the young mathematicians at the 12th Heidelberg Laureate Forum, has already come to pass:
>> Speakers described a future in which superhuman AI mathematicians transcend human knowledge and capabilities: forming conjectures, searching solution spaces, proving conjectures, and finally verifying the proofs and generalizing the results, all without human involvement.
Hold the press for that is already happening: Gauss, the autonomous agent for autoformilization, is already capable of running completely autonomously with "only a paper as input"!
This is not serious. It's some kind of over-exaggerated mumbo-jumbo that fails to impart any useful information and makes it impossible to tell what advances have really been made and where things still can go. But perhaps that's exactly the point? Unbelievable.