QuesnayJr

6 ms·

1.
by QuesnayJr 4d ago
This is exactly backwards. Mathematics predates the idea of formal proof by millenia. The purpose of proofs since Euclid is to explain to your fellow human why something is true. The idea that the purpose of math is formal proof alone is
2.
by QuesnayJr 4d ago
I think it's possible that it will play out that way, and that it's just too soon to see it. Tao was very optimistic about AI up until a few months ago, and I think what's changed is that an AI generated proof isn't tha
3.
by QuesnayJr 5d ago
If it's a counterexample to BSD, that would be pretty surprising. It would also be a considerably more impressive achievement, because experts had mostly shifted to Navier-Stokes regularity being false, while as far as I know almost ev
4.
by QuesnayJr 8d ago
I wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.
5.
by QuesnayJr 8d ago
I brought this up here at HN, and in the ensuing discussion Buzzard himself replied saying he was somewhat joking ( https://news.ycombinator.com/item?id=49011950 ).
6.
by QuesnayJr 8d ago
I'm not moving the goalposts. I haven't heard anyone, ever, refer to the Navier-Stokes problem as a top 3 problem in mathematics. People were saying that they thought the solution was in reach a few years ago, before AI was at a
7.
by QuesnayJr 8d ago
We've heard from Buckmaster, who says that they demanded a condition of cutting Alpöge of all credit. If true, it doesn't make them look too good.
8.
by QuesnayJr 8d ago
It seems like this is going to be a PR nightmare, because they are now competing with their own customers. If you're using an LLM to help with your bright idea to cure cancer, you're going to have second thoughts about relying on
9.
by QuesnayJr 8d ago
Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.
10.
by QuesnayJr 8d ago
Of the seven Millenium problems, Navier-Stokes was the one most thought to be in reach. I'm not sure what the top 3 problems are. You can make a case for the Riemann Hypothesis and P != NP, but I'm not sure what #3 would be. May
11.
by QuesnayJr 8d ago
This is pedantic, but isn't only Josaphat the Buddha?
12.
by QuesnayJr 10d ago
"Descriptive set theory" is a good starting point, though it's the bulk of what set theorists in general do. It's true that there's an infinite possible set of axioms. It does seem that the types of axioms that hav
13.
by QuesnayJr 10d ago
I don't see how you came to that conclusion, since I'm telling you the actual state of play. There's a big literature on what results require the Axiom of Choice, for example. (The book Handbook of Analysis and Its Foundati
14.
by QuesnayJr 10d ago
I'm sure AI could contribute to this, but this is already a well-developed field of mathematics, and most of the consequences of additional axioms have been worked out. (The most productive hypothesis has been what's called &quot
15.
by QuesnayJr 12d ago
It wasn't clear that LLMs were up to a Lean translation task of this scale until now. The background required to formalize the FLT proof was tremendous, so many people assumed we would have to wait until all of that was formalized in
16.
by QuesnayJr 12d ago
Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).
17.
by QuesnayJr 12d ago
Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.
18.
by QuesnayJr 12d ago
Holy shit. The proof of FLT is a giant detour through several different areas of mathematics, so formalizing it is a lot of work. An interesting next target would be formalizing the classification of finite simple groups. The original pro
19.
by QuesnayJr 17d ago
I was thinking about trying this exact problem with AI. I missed that it had already been solved. It's not that surprising that someone else already tried it. What's surprising is that open problems get solved so quickly now th
20.
by QuesnayJr 18d ago
Most of what people think about as part of the Arthur myth are from literary sources, like Lancelot, the Knights of the Round Table, or the Grail quest.
21.
by QuesnayJr 18d ago
Mallory's Morte d'Arthur. Most of the Arthur "myth" is deliberately constructed fiction by specific authors, rather than folk myths.
22.
by QuesnayJr 27d ago
As ducttapecrown said in their comment, you can define an addition on points on elliptic curves. (You can think of an elliptic curve as a cubic equation on the plane, so if you take a line that goes through two points, it will go through a
23.
by QuesnayJr 1mo ago
If you allow negative integers, you get negative exponents. To accomodate negative exponents, you can expand the domain again, to rational numbers. If you allow rational numbers, then you have to allow rational exponents, which means you
24.
by QuesnayJr 1mo ago
As it stands now, the frontier models can prove theorems where the techniques exist in the literature, which it knows better than anyone who's ever lived and won't quit where a human would. There's no way to know if that&#x2
25.
by QuesnayJr 1mo ago
You remember correctly. His result is a special case of Langlands.
26.
by QuesnayJr 2mo ago
Your reply isn't a response to the comment, but rather a general expression of antipathy towards mathematicians, who are apparently fatcats who have fancy lifestyles. OpenAI sat on the results so they could drop 10 at a time. It'
27.
by QuesnayJr 2mo ago
They are more than a strong student could achieve. I'm not equally familiar with the problems, but the ones I'm familiar with, if a student solved them people would be thinking "that's someone on track to win the Fields
28.
by QuesnayJr 2mo ago
The ones I'm familiar with are big breakthroughs, but they are both counterexamples. Examples have an advantage in that once you have the example in hand and a sketch of the proof (which they have provided), then an expert can probabl
29.
by QuesnayJr 2mo ago
The Maxwell conjecture was a conjecture in theoretical physics (though not a particularly important one)
30.
by QuesnayJr 2mo ago
Mostly the significance of a conjecture is that we don't know the answer. A conjecture is successfully resolved if it proven or disproven. (In fact, of the three big conjectures to be resolved in the past couple of weeks, one was pro

More ›