logoalt Hacker News

DoctorOetkerlast Friday at 9:48 PM4 repliesview on HN

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.


Replies

Enginerrrdlast Friday at 10:40 PM

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.

show 4 replies
gerdesjlast Friday at 11:36 PM

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.

fourier456last Saturday at 1:52 AM

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-a5c78fb10d...

refulgentislast Saturday at 12:38 AM

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

show 1 reply