auggierose

3 ms·

1.
by auggierose 6d ago
Intelligence does not seem to be magic either, as LLMs are proving now. It is indeed a waste of time to argue that LLMs are not intelligent in their own way, they obviously are. If Navier Stokes doesn't convince you, nothing will. I ju
2.
by auggierose 6d ago
> We (humans) should help humanity flourish. I think this axiom is of course true. But the mistake the article makes, in my opinion, is to try to apply this axiom separately to each domain. If we have this as the over-arching axiom, it
3.
by auggierose 6d ago
That's what I thought also, that is why I posted Tao's version.
4.
by auggierose 6d ago
I am shocked how people can deny that solving Navier Stokes requires some sort of intelligence. Even Doctorow talks of "brute-forcing" a solution. Brute-forcing leads to combinatorial explosion, so there must be something more g
5.
Why do we need human mathematicians anymore?(terrytao.wordpress.com)
275 points by auggierose 6d ago|328 comments
6.
by auggierose 8d ago
I wouldn't use SPARK either, and rather develop my own approach. The problem isn't that the proof has 400 lines of code, every modern system has large proofs (Isabelle/HOL, Lean, etc.) My latest formal proof has over 50K line
7.
by auggierose 12d ago
They do have Fields medal winners among their staff.
8.
by auggierose 12d ago
His wife just died, so he might not be interested in that currently. On the other hand, he can probably use the distraction.
9.
by auggierose 12d ago
Amen.
10.
by auggierose 13d ago
> There is a point in distinguished a formal proof from an intelligible one, Fine, do that if you want. What you cannot do is call a logical and formal proof of a problem not solving the problem in mathematics. That is absurd, and math
11.
by auggierose 13d ago
Here is what they are saying: 1. AI really did solve a problem in mathematics. The first assumption is wrong because to really solve a mathematical problem, providing a mere answer (even if formally certified) is not suff
12.
by auggierose 13d ago
It is not that nicely written.
13.
by auggierose 13d ago
it is not his rejection, this is a guest article written by two other people
14.
by auggierose 13d ago
The article is eloquent and nicely written, and it is also wrong. To say that "1. AI really did solve a problem in mathematics." is wrong, is just wrong. No matter how nice and eloquent you try to explain it afterwards.
15.
by auggierose 13d ago
I don't disagree with you here. But what does "broken" mean? What is "cheating", and is it ever allowed? And maybe you are not only going through your existing training data, but generate training data specifically
16.
by auggierose 13d ago
You funded it before with your tax dollars, and it was already a hobby at this point. Mathematicians do what they do because it is fun. Well-paid-for fun, if they were able to get tenured.
17.
by auggierose 13d ago
Well, in order to do anything, it is good to know what you want to achieve. How do you align the reward signal? You align it so that you can differentiate between persistence and morality, because that is the goal. This is not something you
18.
by auggierose 13d ago
I think it makes a big difference, as persistence and morality are two entirely different things, that need to be trained for differently. If you think of it in human terms: many people don't mind doing immoral things to get what they
19.
by auggierose 13d ago
The problem is, you don't know if it is unsolvable for you for sure until you've tried everything you can think of. These models are quite persistent in going for a solution. This is not about persistence, it is about morals.
20.
by auggierose 14d ago
Or you could just give me a sensible definition.
21.
by auggierose 14d ago
Still waiting for a definition. People giving nonsense reviews is a feature of the peer review system though, yes.
22.
by auggierose 14d ago
I know that it doesn't work.
23.
by auggierose 14d ago
Yes, for a reason, but not a reasonable reason, but the same reason you have for your comment: you just don’t know any better.
24.
by auggierose 14d ago
Yeah, that sounds like it is in the interest of everyone. Not.
25.
by auggierose 14d ago
The main problem is a social and economic one: while digging, someone needs to pay you, and what incentive does anyone have to do that? Before, you could say, Fermat!, give me a million to formalise it, and share a bit of the glamour. There
26.
by auggierose 14d ago
> Peer in peer-reviewed is a logical coherent and functional definition with answers. What is the definition? If you tell me that, then I might be able to tell you if it is logical coherent and functional, I have a PhD in computational l
27.
by auggierose 14d ago
Very interesting analysis. I was just reading this announcement, and thinking, that is the most pointless thing I've ever read. What are they trying to achieve with it? Your comment explains it.
28.
by auggierose 14d ago
Accepted by whom? Peer-reviewed by whom? I guess these little questions are what this article is really about.
29.
by auggierose 14d ago
The Lean proof is published, you can download it. The clock definitely is ticking. Edit: Oh, didn't see the "qualifying outlet" condition. But Poincare was ever just put on arXiv, so arXiv must count as well.
30.
by auggierose 14d ago
Yes. Mathematicians don't really get logic, and Tao is no exception.

More ›