awesome, thanks!

How do you gain confidence that your theorem actually applies to your code?

My Rocq setup directly reads my actual code. And I fuzz my semantic models against the real machine.

Is this closed source?

Yeah. I've been considering asking my boss about open-sourcing it but I'm probably gonna flesh it out a lot more first.

What is this meant to do? You're just showing that OpenAI didnt post a Lean proof that Lean/nanoda doesn't really accept?

I don't think this is a reasonable take at all. Most work on maths has no real benefit other than to further human understanding of maths - it's more like an art. Nothing is gained from OpenAI solving all these problems but taking jobs from mathematicians. Other than advertising for OpenAI at least. It could not be more different from having AI work on disease research etc.

> Most work on maths has no real benefit other than to further human understanding of maths - it's more like an art.

It's been a while since I was reminded of this xkcd: https://xkcd.com/435/

Most math isn't just proving novel famous results. Just like most of software engineering isn't writing code.

There's a project called lean4lean that implements lean in lean. I guess ideally, if you had a kernel optimisation idea you could do a copy of the Lean model lean4lean has created, add the optimisation, then prove your new lean is equivalent in terms of what it can prove to the old lean

yes and it has for a very long time. Stockfish took the neural net approach after AlphaZero showed it was a good idea as all modern chess engines have

They basically replaced the static position evaluation function with a NN approach and kept the rest of the tree search mostly intact.

I ran fishtest on an old cluster for a while. Was nice to watch the stockfish team methodically improving things. Basically, every commit has to show it can beat the main branch before it gets merged.