Curious if the authors are hanging around here and how they feel about the recent Leiden Statement. (Late in the article it’s clear that this is at least partially a publicity effort around a new AI math tool, if I’m reading it correctly.)
On a personal level I’m very excited about AI getting good at math, but I’m a consumer of math, not a creator. My job gets easier as AI gets better on this front, so I can’t fully empathize with mathematicians who feel threatened or are worried about the sanctity of the discipline.
I am a producer of math. But I feel two ways about AI math.
First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.
Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!
I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.
A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.
As someone who has been both a mathematician and a software engineer at different points, my prediction for mathematics may be biased, but I think it's still true: research mathematics and software engineering are going to effectively merge, very slowly at first, then rapidly, as if on another exponential that the world is only just starting to discover exists.
Natural language proofs are beautiful, but require human mathematicians and collaborators to have spent a lifetime becoming capable of producing their own material and reviewing the material of others.
Right now, formal proofs are machine-checkable -- so that any competent engineer could run a Lean checker at home without understanding research mathematics -- but working manually in Lean requires even more special expertise than the above.
AI formal methods will let creative, high-agency, visionary people throughout the world contribute to mathematics with verifiably correct proofs without needing to pass through the same gauntlet as present-day mathematicians. At first, that will feel like a loss. Some will call it slop. Some will grieve the loss of the artisinal elegance of slowly hand-crafting a deep paper over months or years. But then the breakthroughs will come. As a result of so many more brilliant people contributing at a higher rate than ever before in history, stunning conceptual bridges and dramatic new constructions and techniques will start popping up. This will change the subject forever. It will elevate it to a point where doing hand-crafted artisanal proofs will feel antiquated and altogether far too slow for any serious work.
Curious if the authors are hanging around here and how they feel about the recent Leiden Statement. (Late in the article it’s clear that this is at least partially a publicity effort around a new AI math tool, if I’m reading it correctly.)
On a personal level I’m very excited about AI getting good at math, but I’m a consumer of math, not a creator. My job gets easier as AI gets better on this front, so I can’t fully empathize with mathematicians who feel threatened or are worried about the sanctity of the discipline.
I am a producer of math. But I feel two ways about AI math.
First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.
Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!
I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.
A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.
As someone who has been both a mathematician and a software engineer at different points, my prediction for mathematics may be biased, but I think it's still true: research mathematics and software engineering are going to effectively merge, very slowly at first, then rapidly, as if on another exponential that the world is only just starting to discover exists.
Natural language proofs are beautiful, but require human mathematicians and collaborators to have spent a lifetime becoming capable of producing their own material and reviewing the material of others.
Right now, formal proofs are machine-checkable -- so that any competent engineer could run a Lean checker at home without understanding research mathematics -- but working manually in Lean requires even more special expertise than the above.
AI formal methods will let creative, high-agency, visionary people throughout the world contribute to mathematics with verifiably correct proofs without needing to pass through the same gauntlet as present-day mathematicians. At first, that will feel like a loss. Some will call it slop. Some will grieve the loss of the artisinal elegance of slowly hand-crafting a deep paper over months or years. But then the breakthroughs will come. As a result of so many more brilliant people contributing at a higher rate than ever before in history, stunning conceptual bridges and dramatic new constructions and techniques will start popping up. This will change the subject forever. It will elevate it to a point where doing hand-crafted artisanal proofs will feel antiquated and altogether far too slow for any serious work.