alt Hacker NewsYou 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.
Replies
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.
>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.
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".
> 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.