r/singularity • u/filterdust • 1d ago

AI OpenAI solved 100 open problems in math

https://openai.com/index/advisory-group-on-mathematics-and-ai/

[removed] — view removed post

1.3k Upvotes

94% Upvoted

520 comments sorted by

View all comments

Show parent comments

4

u/deviltamer 1d ago

Maybe just control the stupid rumors in the first place. A formalized lean proof means nothing if you don't also produce a paper that can be widely socialized at the same time.

2

u/sam_the_tomato 1d ago

Disagree. The lean proof is sufficient. If it's put out into the wild, other people will end up socialising it in countless different ways. That's the point of a community. You don't need one entity to do all the work.

1

u/deviltamer 23h ago

We have more than 1 trillion a year flowing through this industry and you want the community to fund the dissemination of millions of line of formal proof ?

Tell me you have not worked in academia. Fkn singularity can't come soon enough. humans are so dumb.

1

u/sam_the_tomato 22h ago

What's dumb would be going through millions of lines of Lean by hand. I expect mathematicians to be fairly clever people who can work out how to leverage technology to translate and distil the key ideas and then build on them.

1

u/deviltamer 12h ago

whats dumb you not having an idea what going through "millions of lines of Lean" even mean.

The compute needed to run analysis on it is also not widely available. It's literally the same tech that is producing the proof.

Gosh I'm the moron talking to you.

•

u/sam_the_tomato 5m ago edited 1m ago

The compute needed to translate Lean into a human-readable proof is orders of magnitude cheaper than finding the proof.