6 ms·

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

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 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo ago
        Deduce. So your #2.
        DoctorOetker 10mo ago
        Of course a machine can verify each step of a proof, but that formal proof must be first presented to the machine.
        crazygringo 10mo 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 10mo 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.
        crazygringo 10mo ago
        > Theres nothing difficult about formalizing a proof you understand. What are you basing that on? It's completely false. If that were true, we would have machine proofs of basically everything we have published proofs for. Every published mathematical paper would be accompanied by with its machine-provable version. But it's not, because the kind of proof suitable for academic publication can easily take multiple years to formalize to the degree it can be verified by computer. Yes of course a large part depends on formalizing prior authors' work, but both are hard -- the prior stuff and your new stuff. Your assertion that there's "nothing difficult" is contradicted by all the mathematicians I know.
  - pxc 10mo ago
    For one, some geometric proofs by construction can literally involve pictures rather than statements, right?
    - DoctorOetker 10mo ago
      Sure the history of mathematics used many alternative conceptions of "proof". The problem is that such constructions were later found to be full of hidden assumptions. Like working in a plane vs on a spherical surface etc. The advantage of systems like MetaMath are: 1. prover and verifier are essentially separate code bases, indeed the MM prover is essentially absent, its up to humans or other pieces of software to generate proofs. The database just contains explicit axioms, definitions, theorems claims, with proofs for each theorem. The verifier is a minimalistic routine with a minimum amount of lines of code (basically substitution maps, with strict conditions). The proof is a concrete object, a finite list of steps. 2. None of the axioms are hardcoded or optimized, like they tend to be in proof systems where proof search and verification are intermixed, forcing axioms upon the user.
  - variaga 10mo ago
    >Do you just mean that we must assume something to get the ball rolling They're called "axioms"
almostgotcaught 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo ago
  [deleted]
- amanaplanacanal 10mo ago
  Do you have the weekend free? Perhaps you can take this new proof and show us how it is done.
  - DoctorOetker 10mo 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.

bmitc 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo ago
      Deduce. So your #2.
      - DoctorOetker 10mo ago
        Of course a machine can verify each step of a proof, but that formal proof must be first presented to the machine.
        crazygringo 10mo 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 10mo 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.
        crazygringo 10mo ago
        > Theres nothing difficult about formalizing a proof you understand. What are you basing that on? It's completely false. If that were true, we would have machine proofs of basically everything we have published proofs for. Every published mathematical paper would be accompanied by with its machine-provable version. But it's not, because the kind of proof suitable for academic publication can easily take multiple years to formalize to the degree it can be verified by computer. Yes of course a large part depends on formalizing prior authors' work, but both are hard -- the prior stuff and your new stuff. Your assertion that there's "nothing difficult" is contradicted by all the mathematicians I know.
- pxc 10mo ago
  For one, some geometric proofs by construction can literally involve pictures rather than statements, right?
  - DoctorOetker 10mo ago
    Sure the history of mathematics used many alternative conceptions of "proof". The problem is that such constructions were later found to be full of hidden assumptions. Like working in a plane vs on a spherical surface etc. The advantage of systems like MetaMath are: 1. prover and verifier are essentially separate code bases, indeed the MM prover is essentially absent, its up to humans or other pieces of software to generate proofs. The database just contains explicit axioms, definitions, theorems claims, with proofs for each theorem. The verifier is a minimalistic routine with a minimum amount of lines of code (basically substitution maps, with strict conditions). The proof is a concrete object, a finite list of steps. 2. None of the axioms are hardcoded or optimized, like they tend to be in proof systems where proof search and verification are intermixed, forcing axioms upon the user.
- variaga 10mo ago
  >Do you just mean that we must assume something to get the ball rolling They're called "axioms"

almostgotcaught 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo 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 10mo ago
[deleted]
amanaplanacanal 10mo ago
Do you have the weekend free? Perhaps you can take this new proof and show us how it is done.
- DoctorOetker 10mo 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.