auggierose

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 lines of proof. That's why AI is such a useful tool.

They do have Fields medal winners among their staff.

His wife just died, so he might not be interested in that currently. On the other hand, he can probably use the distraction.

Amen.

> 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 mathematicians that insist on this are absurd, too. Note that Tao didn't say this, but two guests.

I understand that you might want more than a formal proof generated by a machine, just like I want fries with my steak. But saying that the steak is not food, is just ridiculous.

You are not further along in the discussion, you are having the wrong discussion. What is at stake here is nothing less than the question: Is mathematics subjective or objective? This mathematician thinks it is objective.

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 sufficient.

Yes, it is sufficient. To say otherwise is just goalpost shifting because you don't like the answer.

    There are, in fact, two notions of proof: a logical
    notion and an intelligible notion.

Wrong again, the only real notion of proof is logical. It is not even possible to say exactly what an "intelligible" notion would be, because that would make it logical.

I would be very surprised if Tao couldn't extract a proof that he understands within a few months out of the formal proof. I would compare this to understanding a difficult proof in some math journal.

In the end, all of this forth and back does not matter. A logical proof is a perfectly fine answer, and given that AI can provide that now, this is the future.

It is not that nicely written.

it is not his rejection, this is a guest article written by two other people

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.

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 to make clear to the model that .... what exactly?

If you don't know how persistence and morality interact, and you don't have a theory in place for this, I don't have confidence you can properly supervise the training data. Which is how we arrived at the current situation.

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.

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 should let the AI figure out by itself, because when it does, lying and cheating agents will be the result, just like humans have figured that out for themselves.

This can be as simple as rewarding moral behaviour and penalising immoral behaviour in your training, but how is that interacting with persistence? Maybe a white lie is fine sometimes in order to achieve your goal? So, when designing your training, you will need to answer for yourself how persistence interacts with morality. That is not something you can outsource to machine learning. Or rather, you can, but then you get lying and cheating agents.

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 want.

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.

Or you could just give me a sensible definition.

Still waiting for a definition. People giving nonsense reviews is a feature of the peer review system though, yes.

I know that it doesn't work.

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.

Yeah, that sounds like it is in the interest of everyone. Not.

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 is no glamour in digging.

> 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 logic.

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.

Accepted by whom? Peer-reviewed by whom?

I guess these little questions are what this article is really about.

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.

Yes. Mathematicians don't really get logic, and Tao is no exception.

So, is that basically the Taj Mahal of counter examples?

Funny that the rumour about the big Anthropic announcement had nothing to do with Navier-Stokes. It was about the formalisation of Fermat.

That was Anthropic.

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 what kind of mathematics appears when you actually try to formalise your applications properly. It pretty much includes everything that is thought of as pure mathematics today, and much more.

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! It will be used to improve implementations of proof assistants for a long time.