|
| ▲ | fspeech 4 hours ago | parent | next [-] |
| I think it would be helpful to people who want to understand what a formalized proof is to read Thomas Hales on this: https://www.math.stonybrook.edu/~bishop/classes/math536.S24/... He spent years formalizing his sphere packing theorem because the proof (human produced) was already beyond the ability of peer reviews. Now his formalization effort likely can be easily reproduced by a model. However one should read his experience about what a formal proof is: often the problem is the statement not the proof. The example he gave is the Jordan curve theorem. It's actually quite challenging to formalize the concept of a planar curve (there are space filling curves). So it is not necessary that someone can look at a formal statement and say aha it is about a planar curve, unlike FLT where there is not much problem in recognizing what the statement is about. |
| |
| ▲ | fspeech an hour ago | parent [-] | | Fun challenge: find the formal definition of simple_closed_curve in the essay and tell me if you believe you learned anything about a planar curve. BTW the essay is eminently readable for anyone interested in math. Hales wrote it in favor of formalized math and to educate his peers and students about it. |
|
|
| ▲ | binlog 4 hours ago | parent | prev | next [-] |
| What makes you think no one can comprehend this? It has been less than an hour since it dropped and there is already a ton of online chatter from people explaining the results, pointing out their favorites and more. Some of it is happening on this very thread. |
| |
| ▲ | fspeech 4 hours ago | parent [-] | | I didn't say that. I am responding to "In a way this is probably 50-100 years of math progress by humans." I am actually very excited about AI proof and I am working overtime in my own way to try to comprehend as much as I can. |
|
|
| ▲ | gpt5 4 hours ago | parent | prev | next [-] |
| Math is far more than that. If you can solve prime factorization for example, suddenly you can listen and interfere with almost every private conversation on the internet. We are not far away from the moment where these models will be restricted, and sharing the results will be done more carefully. |
| |
| ▲ | fspeech 4 hours ago | parent [-] | | This doesn't contradict what I said. But I do appreciate the fact AI can produce side effects not just humans. I made it sound like only human knowledges matter. That's too narrow. |
|
|
| ▲ | fspeech 4 hours ago | parent | prev | next [-] |
| Another way to state this: math theorems are like programs without side effects; it is immaterial whether a program without side effects is ever run. We study math for the side effects: it changes how we organize our thoughts. |
|
| ▲ | 4 hours ago | parent | prev | next [-] |
| [deleted] |
|
| ▲ | yieldcrv 4 hours ago | parent | prev | next [-] |
| Academics have been treating it that way because they had no other choice, and its been a waste of everyone’s time and often times taxpayer resources Look at that, taxpayer funding was cut and a private sector solution came in just the nick of time, far accelerating the holding patterns we’ve been in for decades Humanity doesn’t need all iterations towards the blueprints, the blueprint is good enough, we all stand on the shoulders of giants |
| |
| ▲ | fspeech 3 hours ago | parent [-] | | If you actually looked into how agents proved FLT you would be even more amazed by the fellow human beings who are able to keep all this in their heads! I for one can only begin to grasp the scope with AI and scripts. |
|
|
| ▲ | caaqil 4 hours ago | parent | prev | next [-] |
| > until we can comprehend it there really isn't much progress Who is "we" here exactly? |
| |
| ▲ | fspeech 4 hours ago | parent [-] | | Whoever wants to study the result. | | |
| ▲ | caaqil 4 hours ago | parent [-] | | > Whoever wants to study the result. Right. Before all the AI disruption, pure Math traditionally welcomed anyone who wanted to study its esoteric proofs, right? I remember all the excitement of the average Math enthusiast casually reading Wiles' proof over coffee. Bottom line is, the relevant people can still understand the generated proofs. The disorienting part is they are a little slower than they'd like, but they'll get there. | | |
| ▲ | fspeech 3 hours ago | parent [-] | | AI is very helpful with understanding AI proofs. Agent swarms produce messy proofs overall but locally they are excellent and can teach anyone who wants to study them. No one controls math (in a material way funders do control an aspect of practicing math). Still, theorems are already true before we prove them. The difference a proof makes is whether it convinces the reader. |
|
|
|
|
| ▲ | warkdarrior 4 hours ago | parent | prev | next [-] |
| > Math theorems are tautologies Proven math theorems are tautologies. |
| |
| ▲ | fspeech 4 hours ago | parent | next [-] | | FLT was no less a tautology before it was proved. We just weren't sure about it. Proofs only change us, not math. | |
| ▲ | fspeech 4 hours ago | parent | prev [-] | | True. |
|
|
| ▲ | gizmodo59 4 hours ago | parent | prev [-] |
| >So until we can comprehend it there really isn't much progress. Not really? We are at a point if an AI today can solve it, it can be stepping stone of understanding something deeper to tomorrows AI and it continues. Sort of like our limitations doesn't matter. Obviously there are many scenarios in this recursive loop but saying it isn't much progress is not how I view this as |
| |
| ▲ | le-mark 3 hours ago | parent | next [-] | | But who will ask the questions or direct further research when humans no longer understand the state of mathematics? Llms lack the drive for homeostasis combined with the evolutionary drive for survival and reproduction thus to direct themselves. They could very easily spend an eternity down a rabbit hole when the warp drive equation was fairly close on another branch. | |
| ▲ | fspeech 4 hours ago | parent | prev [-] | | If it changes how we think then yes it has an effect. |
|
