auggierose

4 ms·

31.
by auggierose 1mo ago
So, is that basically the Taj Mahal of counter examples?
32.
by auggierose 1mo ago
Funny that the rumour about the big Anthropic announcement had nothing to do with Navier-Stokes. It was about the formalisation of Fermat.
33.
by auggierose 1mo ago
That was Anthropic.
34.
by auggierose 1mo 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
35.
by auggierose 1mo 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!
36.
by auggierose 1mo 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
37.
by auggierose 1mo ago
Maybe society has the wrong values. Maybe society needs to rethink incentives. Maybe society is somewhat antisocial.
38.
by auggierose 1mo 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
39.
by auggierose 1mo 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
40.
by auggierose 1mo ago
I hear you. :-)
41.
by auggierose 2mo ago
> mostly a solved problem > as good as any Mac Yeah, no. If you don't feel or care about the difference, good for you. The rest of us will have to use a mac.
42.
by auggierose 2mo ago
Let me be just for a second here be an intuitionist: not (not M) does not imply M. Everyone can be rich. But not everyone can be Montecito-rich.
43.
by auggierose 2mo ago
That is not a silly point at all. You confuse understanding the mechanics of it with having a theory of why it works. For the physics simulation, physics provides us with the theories which give us the equations underlying the physics simul
44.
by auggierose 2mo ago
I don't care about Montecito. Harry and Meghan apparently neither. Being rich doesn't mean you can do whatever you want. But it means you can choose not to do what you don't want.
45.
by auggierose 2mo ago
I think everyone should become rich. That is the goal of AI, isn't it?
46.
by auggierose 2mo ago
Usually, if you don't understand something in what an AI writes, it is a clear sign that there is a problem hidden somewhere in there. I explicitly always ask wtf exactly it means by something I don't understand, and for sure ther
47.
by auggierose 2mo ago
I don't think anyone wants to be employed. They want the money that comes with employment. If you can make get money without employment, like rich kids, for example, I think most people would prefer that.
48.
by auggierose 2mo ago
Whose requirements?
49.
by auggierose 2mo ago
Does this mean that ChatGPT Desktop will run now also on Intel Macs?
50.
by auggierose 3mo ago
Not sure what your comment has anything to do with my comment, or the comment I replied to. But to answer to your comment: Opus 5 says that Nielsen's critique is nonsense.
51.
by auggierose 3mo ago
Opus 5 says the disproof is wrong.
52.
by auggierose 3mo ago
That's different though. Understanding the spec of Fermat's last theorem is simple. Here, you already need to know some mathematics just to understand the spec.
53.
by auggierose 3mo ago
Because it is more efficient, of course. Same reason why I use Codex/Claude Code for programming, and not only the chat window.
54.
by auggierose 3mo ago
That's fine. This is a statement about yourself, not me.
55.
by auggierose 3mo ago
I am pretty sure you cannot send 1000 high value AI generated emails.
56.
"Fork it or leave": Linus Torvalds fires back at Linux's anti-AI crowd(neowin.net)
5 points by auggierose 3mo ago|1 comments
57.
by auggierose 3mo ago
No, something truly better does not exist yet, but that doesn't mean that it won't. Lean is young compared to Isabelle or Rocq, but actually quite old in absolut terms (and especially in AI terms).
58.
by auggierose 3mo ago
Or we just don't use LEAN but something better.
59.
by auggierose 3mo ago
Which is still a case of the spec being simpler than the implementation (you are after) ;-) Very often, the spec is indeed just a very simple implementation. Often you can make the spec especially simple if there are no constraints on the r
60.
by auggierose 3mo ago
I wouldn’t split it like that. Formal verification is useful in the case that the spec is simpler than the implementation. That’s it. Coming up with simple specs is not necessarily easy. You could say that is kind of what math is about. Th

More ›