7 ms·

It's 2025, if you want to publish grand claims, and you're initially the only one who understands your own proof, publish a machine readable proof in say MetaMa

It's 2025, if you want to publish grand claims, and you're initially the only one who understands your own proof, publish a machine readable proof in say MetaMath's .mm format.

Enginerrrd 11mo ago
You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. Most groundbreaking proofs these days aren’t just cross-discipline but usually involve one or several totally novel techniques. All that to say: I think you’re dramatically underestimating the difficulty involved in this, EVEN if the author(s) were a(n) expert(s) in machine readable mathematics, which is highly UNlikely given that they are necessarily (a) deep expert(s) in at LEAST one other field.
- bmitc 11mo ago
  Plus, mathematics isn't just a giant machine of deductive statements. And the proof checking systems are in their infant stages and require huge amounts of efforts even for simple things.
  - RossBencina 11mo ago
    > mathematics isn't just a giant machine of deductive statements I think the subject at question here is mathematical truth, not "mathematics" whatever that means.
  - sublinear 11mo ago
    > mathematics isn't just a giant machine of deductive statements I know HN can be volatile sometimes, but I sincerely want to hear more about these parts of math that are not pure deductive reasoning. Do you just mean that we must assume something to get the ball rolling, or what?
    - crazygringo 11mo ago
      I think the point was that it's not a machine. Stuff that we can deduce in math with common sense, geometric intuition, etc. can be incredibly difficult to formalize so that a machine can do it.
      - DoctorOetker 11mo ago
        What do you mean with "do it" in "...etc. can be incredibly difficult to formalize so that a machine can do it." ? 1. do it = search for a proof 2. do it = verify a purported proof?
        crazygringo 11mo ago
        Deduce. So your #2.
        DoctorOetker 11mo ago
        Of course a machine can verify each step of a proof, but that formal proof must be first presented to the machine.
        crazygringo 11mo ago
        Right. And I said it's incredibly difficult to formalize so that a machine can do it. I don't understand what you're confused about.
        DoctorOetker 11mo ago
        Theres nothing difficult about formalizing a proof you understand. Formalizing hot garbage supposedly describing a proof can be arbitrarily difficult. The problem is not a missing library. The number of definitions and lemmas indirectly used is often not that much. Most of the time wasted when formalizing is discovering time and time again that prior authors are wasting your time, sometimes with verifiably false assumptions, but the community keeps sending you around to another gap-filling approach.
- almostgotcaught 11mo ago
  > You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. people on hn love making these kinds of declarative statements (the one you responded to, not yours itself) - "for X just do Y" as a kind of dunk on the implied author they're responding to (as if anyone asked them to begin with). they absolutely always grossly exaggerate/underestimate/misrepresent the relevance/value/efficacy of Y for X. usually these declarative statements briskly follow some other post on the frontpage. i work on GPU/AI/compilers and the number of times i'm compelled to say to people on here "do you have any idea how painful/pointless/unnecessary it is to use Y for X?" is embarrassing (for hn). i really don't get even get it - no one can see your number of "likes". twitter i get - fb i get - etc but what are even the incentives for making shit up on here.
  - nospice 11mo ago
    It feels good to be smarter than everyone else. You see your upvotes and that's good enough for an ego boost. Been there, done that. I wish we were a bit more self-critical about this, but it's a tough problem when what brings the community together in the first place is a sense of superiority: prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right?
    - rjh29 11mo ago
      HN is frequently fodder for satire on other forums. Nobody thinks HN users have "refined tastes", or even that they are "smart" for that matter.
      - falseprofit 11mo ago
        Hey, do you mind sharing any of these other forums? I’m trying to make my way up the satire food chain.
    - le-mark 11mo ago
      > prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right? Being pompous and self obsessed requires none of those things.
- DoctorOetker 11mo ago
  >You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. Is it really known to be the frontier as long as its not verified? I would call the act of rigorous verification the acknowledgement of a frontier shift. Consider your favorite dead-end in science, perhaps alchemy, the search for alcahest, the search for the philosophers stone, etc. I think nobody today would pretend these ideas were at the frontier, because today it is collectively identified as pseudoscience, which failed to replicate / verify. If I were the first to place a flag on some mountain, that claim may or may not be true in the eyes of others, but time will tell and others replicating the feat will be able to confirm observation of my flag. As long as no one can verify my claims they are rightfully contentious, and as more and more people are able to verify or invalidate my claims it becomes clear if I did or did not move the frontier.
- DoctorOetker 11mo ago
  One doesn't need to be an expert in machine readable mathematics, to understand how to formalize it to a machine readable form. If one takes the time to read the free book accompanying the metamath software, and re implements it in about a weekend time, you learn to understand how it works internally. Then playing around a little with mmj2 or so you quickly learn how to formalize a proof you understand. If you understand your own proof its easy to formalize it. One doesn't need to be "an expert in machine readable mathematics".
  - deleted 11mo ago
    [deleted]
  - amanaplanacanal 11mo ago
    Do you have the weekend free? Perhaps you can take this new proof and show us how it is done.
    - DoctorOetker 11mo ago
      If one is given an incomplete proof (i.e. where not each step is justified in terms of theorems completely justified before it) there is an amount of bruteforce entropy involved for guessing which intermediate steps weren't jotted down. Of course it takes 20x or more effort if the prover refused to write down certain steps. It even occurs that when pointed out, it takes the original "prover" a lot of time to find a proof for a gap, hence it wasn't originally proven. If I find my own proofs, or if the proof of someone else is clearly written, formalization is not hard at all. Let us assume for the sake of this discussion that Wiles' latest proof for FLT is in fact complete, while his earlier proof wasn't. It took Wiles and his helper more than a weekend to close the gap. Imagine no one had challenged the proof or pointed out this gap. Anyone tasked with formalizing it would face the challenge of trying to figure out which result (incorrectly presumed to be already known) was used in a certain step. The formalizer is in fact finishing an unfinished proof. After succeeding in closing this gap, who else was willing to point at the next gap? There is always some sense of prestige lost when pointing at a "gap" and then observing the original prover(s) close that gap, in a sense they saw how to prove it while the challenger did not. This dynamic is unhealthy. To claim a proof we should expect a complete proof, the burden of proof should lay on the proving claimant not on the verifier.
gerdesj 11mo ago
I am absolutely no expert but I doubt many of the components of this beast are even expressible in anything currently machine readable (perhaps definable is a better word for now). The article clearly states that there are multiple reading groups across the world attempting to get to grips with each small aspect of the ideas involved. That they even attempt this implies to me that the ideas are considered worth studying by some serious players in the field: the group (its way more than just one Fields toting bloke) have enough credibility for that.
refulgentis 11mo ago
You're the top-rated comment, didn't read the article*, posted the most flippant response possible based on whatever couple sentences you didn't understand, and I'll get downvoted for pointing it out, even if I leave out the "I'll get downvoted" part. Really a shame. * there's way more than one person involved here
- DoctorOetker 11mo ago
  But I did read the article! Some random definition of flippant: "not showing a serious or respectful attitude." In my view publishing proofs in 2025 without machine readable proofs is quite flippant yes. We have powerful computation systems, with huge amounts of RAM and storage, yet the bulk does most of mathematics on a computer in the form of... high-tech calligraphy? People are wasting each others time by not using formal verification, to me that is disrespectful. Is pointing out this disrespectful facet of collective behavior disrespectful? For example are people who point out the problems associated with GHG emissions, really being flippant when they point out the flippant behavior of excess emission?
fourier456 11mo ago
I think you have a point. The paper has load bearing reliance on other preprints. I think soon we see a workflow where AI (ChatGPT) can identify precise transitions in the argument that do not require full formalization to falsify. Link - https://chatgpt.com/share/693cc655-ca94-800c-870a-a5c78fb10da1 https://chatgpt.com/share/693cc655-ca94-800c-870a-a5c78fb10d...
- rossjudson 11mo ago
  I did the same thing (roughly) with Gemini 3.0 Pro. Prompt: "Analyze the mathematics in the paper. Find mistakes, note instabilities (if present) and generally criticize as needed." https://gemini.google.com/share/6860fdaea334 https://gemini.google.com/share/6860fdaea334 The mathematics here are far beyond me, but it's interesting that Gemini more or less concurs with chatgpt with respect to "load bearing reliance on other preprints". Gemini's summary (there's much more in the link above that builds up to this): The mathematics is largely robust but relies on heavy "black box" theorems (Iritani's blowup formula, Givental's equivariant mirror symmetry) to bypass difficult geometric identifications in the non-archimedean setting. The primary instability is the lack of a non-archimedean Riemann-Hilbert correspondence, which limits the "enhanced" atoms theory. The core results on cubic fourfolds hold because the specific spectral decomposition (eigenvalues $0, 9, 9\zeta, 9\zeta^2$) is robust and distinct22, but the framework's extension to finer invariants (integral structures) is currently obstructed.

It's 2025, if you want to publish grand claims, and you're initially the only one who understands your own proof, publish a machine readable proof in say MetaMath's .mm format.

Enginerrrd 11mo ago

You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. Most groundbreaking proofs these days aren’t just cross-discipline but usually involve one or several totally novel techniques. All that to say: I think you’re dramatically underestimating the difficulty involved in this, EVEN if the author(s) were a(n) expert(s) in machine readable mathematics, which is highly UNlikely given that they are necessarily (a) deep expert(s) in at LEAST one other field.

bmitc 11mo ago
Plus, mathematics isn't just a giant machine of deductive statements. And the proof checking systems are in their infant stages and require huge amounts of efforts even for simple things.
- RossBencina 11mo ago
  > mathematics isn't just a giant machine of deductive statements I think the subject at question here is mathematical truth, not "mathematics" whatever that means.
- sublinear 11mo ago
  > mathematics isn't just a giant machine of deductive statements I know HN can be volatile sometimes, but I sincerely want to hear more about these parts of math that are not pure deductive reasoning. Do you just mean that we must assume something to get the ball rolling, or what?
  - crazygringo 11mo ago
    I think the point was that it's not a machine. Stuff that we can deduce in math with common sense, geometric intuition, etc. can be incredibly difficult to formalize so that a machine can do it.
    - DoctorOetker 11mo ago
      What do you mean with "do it" in "...etc. can be incredibly difficult to formalize so that a machine can do it." ? 1. do it = search for a proof 2. do it = verify a purported proof?
      - crazygringo 11mo ago
        Deduce. So your #2.
        DoctorOetker 11mo ago
        Of course a machine can verify each step of a proof, but that formal proof must be first presented to the machine.
        crazygringo 11mo ago
        Right. And I said it's incredibly difficult to formalize so that a machine can do it. I don't understand what you're confused about.
        DoctorOetker 11mo ago
        Theres nothing difficult about formalizing a proof you understand. Formalizing hot garbage supposedly describing a proof can be arbitrarily difficult. The problem is not a missing library. The number of definitions and lemmas indirectly used is often not that much. Most of the time wasted when formalizing is discovering time and time again that prior authors are wasting your time, sometimes with verifiably false assumptions, but the community keeps sending you around to another gap-filling approach.
almostgotcaught 11mo ago
> You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. people on hn love making these kinds of declarative statements (the one you responded to, not yours itself) - "for X just do Y" as a kind of dunk on the implied author they're responding to (as if anyone asked them to begin with). they absolutely always grossly exaggerate/underestimate/misrepresent the relevance/value/efficacy of Y for X. usually these declarative statements briskly follow some other post on the frontpage. i work on GPU/AI/compilers and the number of times i'm compelled to say to people on here "do you have any idea how painful/pointless/unnecessary it is to use Y for X?" is embarrassing (for hn). i really don't get even get it - no one can see your number of "likes". twitter i get - fb i get - etc but what are even the incentives for making shit up on here.
- nospice 11mo ago
  It feels good to be smarter than everyone else. You see your upvotes and that's good enough for an ego boost. Been there, done that. I wish we were a bit more self-critical about this, but it's a tough problem when what brings the community together in the first place is a sense of superiority: prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right?
  - rjh29 11mo ago
    HN is frequently fodder for satire on other forums. Nobody thinks HN users have "refined tastes", or even that they are "smart" for that matter.
    - falseprofit 11mo ago
      Hey, do you mind sharing any of these other forums? I’m trying to make my way up the satire food chain.
  - le-mark 11mo ago
    > prestigious schools, high salaries, impressive employers, supposedly refined tastes. We're at the top of the world, right? Being pompous and self obsessed requires none of those things.
DoctorOetker 11mo ago
>You say that like it’s even remotely feasible at the frontier of mathematics and not a monumental group effort to turn even established proofs into such. Is it really known to be the frontier as long as its not verified? I would call the act of rigorous verification the acknowledgement of a frontier shift. Consider your favorite dead-end in science, perhaps alchemy, the search for alcahest, the search for the philosophers stone, etc. I think nobody today would pretend these ideas were at the frontier, because today it is collectively identified as pseudoscience, which failed to replicate / verify. If I were the first to place a flag on some mountain, that claim may or may not be true in the eyes of others, but time will tell and others replicating the feat will be able to confirm observation of my flag. As long as no one can verify my claims they are rightfully contentious, and as more and more people are able to verify or invalidate my claims it becomes clear if I did or did not move the frontier.
DoctorOetker 11mo ago
One doesn't need to be an expert in machine readable mathematics, to understand how to formalize it to a machine readable form. If one takes the time to read the free book accompanying the metamath software, and re implements it in about a weekend time, you learn to understand how it works internally. Then playing around a little with mmj2 or so you quickly learn how to formalize a proof you understand. If you understand your own proof its easy to formalize it. One doesn't need to be "an expert in machine readable mathematics".
- deleted 11mo ago
  [deleted]
- amanaplanacanal 11mo ago
  Do you have the weekend free? Perhaps you can take this new proof and show us how it is done.
  - DoctorOetker 11mo ago
    If one is given an incomplete proof (i.e. where not each step is justified in terms of theorems completely justified before it) there is an amount of bruteforce entropy involved for guessing which intermediate steps weren't jotted down. Of course it takes 20x or more effort if the prover refused to write down certain steps. It even occurs that when pointed out, it takes the original "prover" a lot of time to find a proof for a gap, hence it wasn't originally proven. If I find my own proofs, or if the proof of someone else is clearly written, formalization is not hard at all. Let us assume for the sake of this discussion that Wiles' latest proof for FLT is in fact complete, while his earlier proof wasn't. It took Wiles and his helper more than a weekend to close the gap. Imagine no one had challenged the proof or pointed out this gap. Anyone tasked with formalizing it would face the challenge of trying to figure out which result (incorrectly presumed to be already known) was used in a certain step. The formalizer is in fact finishing an unfinished proof. After succeeding in closing this gap, who else was willing to point at the next gap? There is always some sense of prestige lost when pointing at a "gap" and then observing the original prover(s) close that gap, in a sense they saw how to prove it while the challenger did not. This dynamic is unhealthy. To claim a proof we should expect a complete proof, the burden of proof should lay on the proving claimant not on the verifier.

gerdesj 11mo ago

I am absolutely no expert but I doubt many of the components of this beast are even expressible in anything currently machine readable (perhaps definable is a better word for now). The article clearly states that there are multiple reading groups across the world attempting to get to grips with each small aspect of the ideas involved. That they even attempt this implies to me that the ideas are considered worth studying by some serious players in the field: the group (its way more than just one Fields toting bloke) have enough credibility for that.

refulgentis 11mo ago

You're the top-rated comment, didn't read the article*, posted the most flippant response possible based on whatever couple sentences you didn't understand, and I'll get downvoted for pointing it out, even if I leave out the "I'll get downvoted" part. Really a shame. * there's way more than one person involved here

DoctorOetker 11mo ago
But I did read the article! Some random definition of flippant: "not showing a serious or respectful attitude." In my view publishing proofs in 2025 without machine readable proofs is quite flippant yes. We have powerful computation systems, with huge amounts of RAM and storage, yet the bulk does most of mathematics on a computer in the form of... high-tech calligraphy? People are wasting each others time by not using formal verification, to me that is disrespectful. Is pointing out this disrespectful facet of collective behavior disrespectful? For example are people who point out the problems associated with GHG emissions, really being flippant when they point out the flippant behavior of excess emission?

fourier456 11mo ago

I think you have a point. The paper has load bearing reliance on other preprints. I think soon we see a workflow where AI (ChatGPT) can identify precise transitions in the argument that do not require full formalization to falsify. Link - https://chatgpt.com/share/693cc655-ca94-800c-870a-a5c78fb10da1 https://chatgpt.com/share/693cc655-ca94-800c-870a-a5c78fb10d...

rossjudson 11mo ago
I did the same thing (roughly) with Gemini 3.0 Pro. Prompt: "Analyze the mathematics in the paper. Find mistakes, note instabilities (if present) and generally criticize as needed." https://gemini.google.com/share/6860fdaea334 https://gemini.google.com/share/6860fdaea334 The mathematics here are far beyond me, but it's interesting that Gemini more or less concurs with chatgpt with respect to "load bearing reliance on other preprints". Gemini's summary (there's much more in the link above that builds up to this): The mathematics is largely robust but relies on heavy "black box" theorems (Iritani's blowup formula, Givental's equivariant mirror symmetry) to bypass difficult geometric identifications in the non-archimedean setting. The primary instability is the lack of a non-archimedean Riemann-Hilbert correspondence, which limits the "enhanced" atoms theory. The core results on cubic fourfolds hold because the specific spectral decomposition (eigenvalues $0, 9, 9\zeta, 9\zeta^2$) is robust and distinct22, but the framework's extension to finer invariants (integral structures) is currently obstructed.