auggierose

6 ms·

1.
by auggierose 5d 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
2.
by auggierose 5d 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
3.
by auggierose 5d ago
It is not that nicely written.
4.
by auggierose 5d ago
it is not his rejection, this is a guest article written by two other people
5.
by auggierose 5d 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.
6.
by auggierose 5d 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
7.
by auggierose 5d 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.
8.
by auggierose 5d 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
9.
by auggierose 6d 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
10.
by auggierose 6d 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.
11.
by auggierose 6d ago
Or you could just give me a sensible definition.
12.
by auggierose 6d ago
Still waiting for a definition. People giving nonsense reviews is a feature of the peer review system though, yes.
13.
by auggierose 6d ago
I know that it doesn't work.
14.
by auggierose 7d 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.
15.
by auggierose 7d ago
Yeah, that sounds like it is in the interest of everyone. Not.
16.
by auggierose 7d 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
17.
by auggierose 7d 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
18.
by auggierose 7d 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.
19.
by auggierose 7d ago
Accepted by whom? Peer-reviewed by whom? I guess these little questions are what this article is really about.
20.
by auggierose 7d 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.
21.
by auggierose 7d ago
Yes. Mathematicians don't really get logic, and Tao is no exception.
22.
by auggierose 10d ago
So, is that basically the Taj Mahal of counter examples?
23.
by auggierose 11d ago
Funny that the rumour about the big Anthropic announcement had nothing to do with Navier-Stokes. It was about the formalisation of Fermat.
24.
by auggierose 12d ago
That was Anthropic.
25.
by auggierose 12d ago
Yes, it has been. And in the form of applied mathematics it will continue to be. It is not so much that pure mathematics disappears, but that in the future there will be just mathematics, and of course it is applied. You would be surprised
26.
by auggierose 13d ago
Yes. But that is a problem for pure mathematics, not for society. I think that pure mathematics is over. At the same time, applied mathematics will probably subsume most of pure mathematics. Fermat's theorem now is applied mathematics!
27.
by auggierose 13d ago
You can say that American society made OpenAI and Anthropic possible. No other current society would have. Suddenly, formalisation of math is becoming cheap. That's not a problem, that's the goal, and it is here much earlier than
28.
by auggierose 13d ago
Maybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.
29.
by auggierose 13d ago
Kevin Buzzard is a mathematician as well, and he thinks it's ok. I am a mathematician, too, and I know it is ok. What I find fascinating is how little mathematicians still know about this. But I am used to that attitude towards interac
30.
by auggierose 14d ago
I don't really know Lean, but I think this means, three axioms on top of their whole type theory machinery, to make it classical. The type theory machinery is the obfuscated encoding of the large set of standard axioms that they don&#x

More ›