QuesnayJr

5 ms·

1.
by QuesnayJr 6d ago
I've already seen this sentiment expressed in the wild.
2.
by QuesnayJr 7d ago
Understanding has been the point of mathematics for millenia. The idea that purpose of math is to produce machine-checkable proofs is an entirely modern idea.
3.
by QuesnayJr 9d ago
I wonder if this is a hint to a more-specific rumor. Weil constructed what are now known as "abelian varieties of Weil type". In low dimensions the Hodge conjecture has been proven for abelian varieties of Weil type, but it&#x27
4.
by QuesnayJr 11d ago
The idea that logic is a branch of mathematics is itself a modern notion. Aristotle's logic was part of the trivium (grammar, rhetoric, and logic) in classical notions of education, while mathematics made up several parts of the quadr
5.
by QuesnayJr 12d ago
If you go to the individual solutions, the text description tells you if it's stable. There's also a slider that allows you to perturb the orbit so you can see for yourself when you perturb it.
6.
by QuesnayJr 13d 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
7.
by QuesnayJr 13d 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
8.
by QuesnayJr 14d 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
9.
by QuesnayJr 18d ago
I wouldn't call it "struggle", but it does seem better at proving "there exists" statements than proving "for all" statements.
10.
by QuesnayJr 18d 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 ).
11.
by QuesnayJr 18d 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
12.
by QuesnayJr 18d 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.
13.
by QuesnayJr 18d 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
14.
by QuesnayJr 18d ago
Someone has to actually check this. I'm guessing OpenAI had someone check it internally, but it's possible to get it wrong.
15.
by QuesnayJr 18d 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
16.
by QuesnayJr 18d ago
This is pedantic, but isn't only Josaphat the Buddha?
17.
by QuesnayJr 19d 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
18.
by QuesnayJr 19d 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
19.
by QuesnayJr 19d 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
20.
by QuesnayJr 22d 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
21.
by QuesnayJr 22d ago
Lean's proofchecker is a big piece of code, so it's possible that it has a bug (and historically has had some).
22.
by QuesnayJr 22d 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.
23.
by QuesnayJr 22d 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
24.
by QuesnayJr 26d 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
25.
by QuesnayJr 28d 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.
26.
by QuesnayJr 28d ago
Mallory's Morte d'Arthur. Most of the Arthur "myth" is deliberately constructed fiction by specific authors, rather than folk myths.
27.
by QuesnayJr 1mo 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
28.
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
29.
by QuesnayJr 2mo 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
30.
by QuesnayJr 2mo ago
You remember correctly. His result is a special case of Langlands.

More ›