YHK - yet another hacker news clone

How to Formalize All of Mathematics

28 points practal 1 hour ago 14 comments

N_Lens 41 minutes ago | parent

Godel would like to talk to you about his “Incompleteness Theorem”

fedeb95 36 minutes ago | parent

Also Chaitin would like a few words.

lioeters 18 minutes ago | parent

The Limits of Mathematics: A Course on Information Theory and Limits of Formal Reasoning - Chaitin, Gregory

https://ia801804.us.archive.org/35/items/A-Z_Library_G-K_Jos... (PDF)

bubbluppugus 29 minutes ago | parent

Yeah which is why I don't have much sympathy for folks like Tao either

The ability to conjure math is practically as endless as time

At some point the outcome is just generation of new visual art in the form of syntax

We can't physically observe the past or future so we can only theorize and simulate; IMO that's the physical phenomena that belies Incompleteness Theorem; from Earth in the relative year of 2026 my view of the universe is fundamentally incomplete. As such all language describing too far either is incomplete always.

It makes any kind of longtermism, religious or agnostic framework espoused by kids of rich academics, empty. We all gonna stick around 10 more generations just to make sure?

Whole lot of educated people are just peddling euphemism for religious conviction they steeped in as kids but hid behind atheist semantics like "Intelligent Design."

dwohnitmok 23 minutes ago | parent

This is irrelevant. The theorems Avigard, Buzzard, et al. are talking about all have natural language proofs already that in theory should be formalizable.

They are not claiming all possible theorems are formalizable. They are claiming to try to formalize all already proven theorems in the mathematics canon.

To the extent the theorems in question are impossible to formalize this means the original proof must be in error.

LPisGood 14 minutes ago | parent

If a theorem has a published proof, it is either formalizable or incorrect.

wslh 14 minutes ago | parent

I understand that, even taking Gödel's results into account, formalization helps us analyze mathematics and can lead to new (non-mechanical) ideas and results.

osculum 39 minutes ago | parent

Hasn’t this been tried already?

infamouscow 37 minutes ago | parent

You might be thinking of the Langlands program

osculum 26 minutes ago | parent

You give me too much credit. I was just being tongue-in-cheek about Principia Mathematica.

transitorykris 17 minutes ago | parent

I like the pragmatic take on AI in mathematics. Running off and proving/formalizing things in incomprehensible ways is marginally useful, and probably harmful for any work that needs to move beyond it. But, there's value in what AI is capable of doing for working mathematicians, when used as a partner.

The genie is out of the bottle though. It's hard to see how there won't be weird and inscrutable branches of mathematics that LLMs build and use effectively _for themselves_, in the same way much of the slop LLMs write in spoken language is really for the consumption of LLMs.

Surely there will be a new kind of research mathematician that's investigating this output in the same way, say, academics in literature read.

stabbles 16 minutes ago | parent

"How to rewrite all software in Rust"

solomonb 5 minutes ago | parent

If we are going to formalize everything can we please do it in the style and spirit of the 1lab? https://1lab.dev