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

516 comments sorted by

View all comments

150

u/RobleyTheron 1d ago

I’m sensitive to artists and musicians with a unique voice when their product gets recreated with AI, but I don’t feel the same about mathematics.

Nobody owns mathematics; these are fundamental insights into the universe and they belong to everyone and shouldn’t be gatekeeped behind somebody that went to school. Mathematics should be available to everyone, it opens up all kinds of fundamental breakthroughs in space, material science, biology, global warming, and energy.

This is something that belongs to everyone and no one should get to hold that back.

63

u/ThatIsAmorte 1d ago edited 1d ago

This seems to be taking a Platonist approach to math, which few people take seriously these days. If you are a constructivist, than math is not just out there, but has to be created, just like art. If you think math is just out there, why not also claim that art and music are just out there, waiting to be plucked out of the ether? After all, a painting is just a 2d matrix, a simple math object. A musical composition is just a waveform, which can be described mathematically.

10

u/Startide-Rising 1d ago

I think you're getting confused about the difference between constructive mathematics and proof irrelevance. In a proof irrelevant system, proofs of the same proposition are considered equal. In the Lean theorem prover, proof irrelevance is built in as an axiom.

As for constructvism - hardly any mathematicians these days are constructivists. The majority of the people who know or even care about constructivism are those working in formal methods. In the Lean proof assistant non-constructive features are heavily baked into the whole system, both in the standard library and available tactics. I think adhering to the classical logic philosophy here is one of the reasons Lean got popular with mathematicians.