6 ms·
AI in mathematics is forcing big questions
- andai 4mo ago[dead]
- tuatoru 4mo ago[flagged]
- tiahura 4mo ago[flagged]
- glouwbug 4mo agoTurns out you have to be Terence Tao to know when an LLM is right or wrong
- gerdesj 4mo ago"I imagine my work could be completed with AI assistance in a matter of days—maybe hours." Would some one with tokens to burn mind checking that statement out and post back. Be sure to use long dashes too.
- paulpauper 4mo agoYeah, so much for AI making mathematicians obsolete.
- bijowo1676 4mo agois the similar statement true for coding as well? i.e. You have to be a good engineer to understand the well generated LLM code and a program
- glouwbug 4mo agoYes, that's the point I'm making
- esafak 4mo agoYou don't have to be as good as the model you are overseeing, but it sure helps, otherwise you will only be able to evaluate partial claims, missing mistakes, and potentially the big picture.
- lubujackson 4mo agoThe article poses if AI will be a tool, a collaborator or an oracle. Why not all 3? 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...
- fn-mote 4mo agoI don’t know about “close”, but there are certainly results in math that are considered deep because they require the use of a “Hard Theorem” at some point. That kind of building on top of something Very Difficult is still possible without understanding the “Very Difficult” part. I’d say a lot of not-amazing math is built by believing the platform works but not being able to built it yourself. I couldn’t build an internal combustion engine or even a plastic box, so maybe there’s nothing wrong with this approach.
- paulpauper 4mo agoIt's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very expensive and propitiatory. They are not like the commercial AI that regular people use. It takes considerable prompting and trial an error to solve even Olympiad/Putnam problems, and tons of work by humans pouring over the results to see if it's correct. For every Erdos problem that captures the headlines, there are many where it failed or untold hours of prompting and token burn to get that result, and manhours verify it.
- ares623 4mo agoBut just imagine... (edit: lol didn't realize the sibling comment below is essentially my comment)
- treyd 4mo agoI don't think you understand the workflow. Terrence Tao has done a lot of work using them in conjunction with LEAN. 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.
- hackermailman 4mo agoAI can't yet come up with any new ideas to make the inductive leap to solve a math problem. New ideas are what get the accolades and using an old idea just means the original author missed something. We are still at the author missed something stage that AI is doing today. It can definitely be a good research assistant though
- NateEag 4mo agoThank you for your comment. 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: https://archive.is/oNCSO https://archive.is/oNCSO So, impressive though the result is, perhaps your claim has more grounds than I had thought.
- fiforpg 4mo agoThe use of computers in mathematics has been somewhat controversial from the very start. 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."
- jackyinger 4mo agoTo bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.
- seanmcc 4mo agoAlmost another layer in the peer review process in the best case right? Just a different kind of peer you have to review.
- therobots927 4mo agoSo… more peer review backlog. That sounds fun. Oh, you want someone to review your paper, Mr phd in mathematics with 20 years of experience? Get in line behind chatGPT.
- wbl 4mo agoLook up the story of Flyspeck for this taking an entire career.
- avaer 4mo agoAs a programmer I definitely get annoyed when I see code and I don't understand what it does. 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.
- cpard 4mo agoHuman mathematicians could become “priests to oracles.” 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.
- therobots927 4mo agoHuman mathematicians could become “priests to oracles.” This is a decidedly anti-enlightenment statement.
- Verdex 4mo agoOkay .. 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."
- kevinten10 4mo ago[flagged]
- therobots927 4mo agoIt’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. 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.
- skipkey 4mo agoI would imagine that in the future AI will be doing proofs in Lean or whatever the successor to it, which gives you a pretty good confidence it’s correct.
- bckgrndrdtn 4mo agoThe future is now. See the article under discussion for some examples.
- jonahx 4mo ago> It would be great if someone could explain to me how AI improves this situation. 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.
- tacomonstrous 4mo ago>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.
- Hasan121212 4mo ago[flagged]
- black_13 4mo ago[dead]
- skybrian 4mo agoHere’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: > 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-economy https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...
- crystal_revenge 4mo ago> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob 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.
- zmgsabst 4mo agoYou didn’t answer why merge it into a library focused on humans developing mathematics though. 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.
- morpheos137 4mo agoMuch can be resolved when it is understood math is discovered not created. AI is a tool. if it makes discovery or proof easier that is still mathematics. A proof stands on its own logic regardless how it is derived. The root concern is how ai may provide uplift for mathematical discovery outside of socially expected channels.
- esafak 4mo agoYou're not concerned about mathematics disappearing as a profession?
- morpheos137 4mo agoIt won't. Did automation cause people to stop working in the textile industry?
- frabcus 4mo agoI only did undergraduate level in Maths, and to me there is a key aesthetic element which makes it created. The choice of axioms to use, the choice of with theorems are interesting. 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.
- auggierose 4mo agoThe truth very much exists, see Gödel's theorems. People get confused by this created/discovered thing. Of course it is discovered. It was there even before you created it. ;-)
- andai 4mo ago>more recently, a new general-purpose AI system from OpenAI disproved an important conjecture in combinatorial geometry. This result would have been worthy of publication in a major mathematics journal if humans had been the authors The quality of the mathematics is a function of who has authored it?
- rirze 4mo agoI think we’re going to find out the hard way that the proofs left to solve are very much not elegant.
- stringfood 4mo agocouldn't God have created a more orderly universe for us? this is ridiculous
- CyborgCabbage 4mo agoI want this on a T-shirt
- strogonoff 4mo agoTo assume that the universe is disorderly presumes knowing some esoteric objective truth about how the universe works. Since the field of natural sciences does not provide that truth (by design), and practices that do aim to provide that truth (metaphysics, religion, etc.) seem to have different versions of it, I would say that there’s a fair chance that the universe is not that disorderly and we just lack better models for describing it.
- layer8 4mo agoI don’t think God has any choice regarding math and logic.
- Verdex 4mo agoThe way I look at it, the absurd complexity that rule systems can get into is a check and punishment for the arrogant and the tyrannical. 'Look I designed these rules myself just follow them and everything will be fine.' Ah but what about this edge case. 'Hm, I guess we can add a few more rules.' Bam, next thing you know it's a Byzantine bureaucratic nightmare any your empire refuses to grow anymore. 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.
- mmooss 4mo agoThere's yet another major issue of the centralization of power and knowledge: > 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?
- nok22kon 4mo agoalways has been 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
- mmooss 4mo agoWhat's always been true is change. We decide our future. Sickness has always been there, but that doesn't mean we can't have a enormous influence on our fates. So much that has been true for millenia we've changed in the last century or three.
- jdw64 4mo agoSomeday, human mathematicians might end up doing proofs for proofs. 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?
- mockerell 4mo agoThat’s an interesting way to think about it. While tests don’t satisfy mathematicians‘ standards for rigor one could instead look at interactive proofs from complexity theory. These are of interest if a problem doesn’t allow for short proofs, i.e. when the problem is not in NP [1]. In your scenario an adapted AI-assisted theorem prover would be the prover, and a mathematician the verifier. [1] https://en.wikipedia.org/wiki/Interactive_proof_system https://en.wikipedia.org/wiki/Interactive_proof_system
- jdw64 4mo agoThank you for explaining my point more logically and coherently. I'll read it over.
- bodzioney 4mo agoInteractive theorem provers are what verifies (or proves) the proof here. This means you don’t even have to look at the actual proof to check its correctness. You just have to make sure the theorem definition is what you wanted (not to say this is trivial) and that no nonsense axioms were defined etc. Now for verifying the theorem prover itself, this is kind of a chicken and the egg problem. We know the mathematical foundations are solid. But to check the implementation of said foundations would require… another theorem prover. In practice, most theorem provers try to make their kernel as small as possible so it can be reasoned about by humans. Coming back to the original topic, mathematics isn’t all proofs though. Someone has to come up with new theories and models. I guess this is what mathematicians would be doing in the future if AI becomes better at proving things than humans. But I could see it narrowing the field, just like it’s doing in others.
- ggm 4mo agoArgument started when 4 colour map proof was machine assisted. So 1976. (Which the fine article says: I remember my dad being in this argument at the time from the comp. sci side, albiet as a mathematicianby training)
- 6thbit 4mo agoI always struggled with my lack of intuition vs that of my peers that had had a more comprehensive ‘math upbringing’. Is direct experience and struggle really the only driver for developing intuition?
- bananaflag 4mo agoI am a mathematician, and I was never the kind to like to struggle by working on problems, but I developed a lot of intuition by 1) thinking deeply about definitions and proofs and why are they this way and not another 2) reading a lot of blogs and expository papers by great mathematicians, even (the more philosophically minded) mathoverflow q&a's (so I absorbed their way of thinking unconsciously). For example, I tell my students to read all 300 of John Baez's This Week's Finds posts [1] and they will deeply understand more math than 99% of their peers. This is not the "standard" advice that usually gets peddled but for me it "worked". [1] https://math.ucr.edu/home/baez/twf.html https://math.ucr.edu/home/baez/twf.html
- lioeters 4mo ago> John Baez's This Week's Finds posts 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.
- guyomes 4mo agoBeyond the technical aspects, this new technology also leads to fundamental social changes. 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.
- dag100 4mo ago> mathematics were one of the rare sciences were great scientists could emerge from any country with a good education system. 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.
- utopiah 4mo agoI'm not a mathematician but AFAICT AI in mathematics only helped for paradigmatic works, either verification of well explained, and even researched, conjectures. Ideas that have been labelled as potentially interesting, are verifiable, and in a well known area. It is already quite useful... but it is NOT about paradigm change. It's not about revolutionary ideas. It's about being able to slightly more efficiently do more of of the same. 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.
- blks 4mo agoIn my field that sometimes involves some applied mathematics, it definitely help with busy work, giving raw ideas or writing some chain in latex so I don’t have to spell everything in details myself in the doc
- jadar 4mo agoIsn’t that somewhat similar to everywhere else AI is being employed? More of the same — just faster? We aren’t getting novel software architecture out of AI, those things are still important, but it does help us rule out bad things (bugs, security vulnerabilities, etc) and help us focus on the important things. In that vein, AI could help mathematicians by ruling things out faster.
- PunchyHamster 4mo agoIs the big quesition same as in other domains, "how to stop AI bros from flooding us from slop that is made only to prove AI can do it too?"
- lioeters 4mo agoNews at 5: Team of corporate mathematicians working for OpenAI rewrites the foundation of mathematics in a billion lines of vibe-coded theorems and proofs that are so complex it's impossible for humans to review or understand. Next generation of children don't need to learn math anymore, they just get a subscription to OpenMath™.
- deleted 4mo ago[deleted]
- deleted 4mo ago[deleted]
- christianbryant 4mo agoReading the article from the perspective of a non-mathematician the line that rang true for me was "I realized they derived joy, satisfaction, and meaning from the long journey toward understanding." My eldest child loves math and her whole life has been chaos except when she is solving math problems. I see that human element in science and I know deep down we need that. 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...
- pfdietz 4mo agoThe big question is: why is government (or society) funding mathematics? What justifies this use of resources? 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?
- lambdacity 4mo agoIt's R&D. If you've listened to machine learning, it's heavily based around manifolds, statistics, linear algebra, learning theory, etc. All of which were once pure math. 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].
- pfdietz 4mo agoYes, those are utility arguments. So don't we get more utility if AI now spews out lots of new math results?
- YeGoblynQueenne 4mo agoI swear, with AI it's got to the point that I read articles in the tech press that sound like blog posts by homeopathy enthusiasts, the way they play fast and loose with facts and fudge technical details. Take the following: >> 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 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.