First I fear slop-math. People producing LLM “proofs” and prose with no value. I do not want to review something the author has spend lies energy on than I will spend reviewing.

Two, I am excited about formal machine-checked proofs. I love formalisation, and if the llm can prove my lemmas I will be a happy camper!

I think my optimism here is coloured by the fact that I am a theory builder, not a problem solver. I will be happy to create beautiful theory, writing (myself) wonderful articles explaining them, but letting the ugly details be formally verified by an LLM.

A problem solver kind of mathematician might feel cheated of all the fun of the llm did all the problem solving.

Yesterday Fable 5 finally solved a non trivial problem I had (after working on it for a few hours), and I went to bed excited. Waking up to find that Fable 5 is not available anymore, I guess I should feel happy I have the code it produced yesterday. But frankly I feel like a child having their candy taken from them.

We need open available models as smart as the current US proprietary ones. If intelligence like that becomes common property, i forsee a better future for human kind!

Being a theory builder more than a problem solver I am excited for the future.

Also excited for fully formalised mathematics to hit main stream!

Recently (last couple of months?) these models are becoming useful tools for mathematicians, because they can solve easier problems more quickly, meaning that one can tackle bigger challenges (but maybe not RH et al) piece by piece.

But, there are still definite limits, where one could expect an expert human to solve things, given time, but models do not. Thus, more intelligence would be nice!

(Joking aside, see sibling threads.)

I gave a high level description of the problems in a sibling thread. They are the kind of small problems which I suppose every researcher has lying around, waiting for them to think about some day. But not the big problem everyone is waiting for to be solved.

My comment was not meant to be a tease – sorry! I assumed there would be other people in a similar situation, who might relate.

I am just testing it on stuff I know intimately myself. I would probably not understand a proof of Collatz if it was dansing in front of me!

These are not Fields medal type problems, nor know difficult/open conjectures. Just small stuff I have collected in my todo list over the years.

I see a lot of people saying they are happy with weaker models, but I am the opposite, I need more strength, more intelligence!

I am quite happy that opus 4.8 can do some medium intelligence problems. And maybe Fable 5 can do some more more of those! I have a lot of problems to solve!

I personally think the, perhaps confusingly named, capability based security models are the way of The Future.

Comments URL: https://news.ycombinator.com/item?id=48387944

Points: 3

# Comments: 1

Speculation: I think we must accept that prompt injection happens, and structure the security of the rest of the system around that. Data given to an LLM becomes an agent, so maybe we must give permissions to this data, instead of to the LLM. Not sure exactly how this would look like in practice!

There is also this blogpost by Amdrej Bauer, which can be seems as exploring how it is to be such such a topos: https://math.andrej.com/2006/03/27/sometimes-all-functions-a...

I think we create mathematics as thought structure in our mind. We can agree on things when we create the same structures. But this structure did not exist prior to creation.

I know of no realm where mathematical objects live except human minds.

No, it seems clear to me that mathematics is a creation of our minds.