Hacker News: mattr03

New comment by mattr03 in "Sharing AI progress in mathematics"

mattr03 — Wed, 07 Oct 2026 02:01:06 +0000

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

New comment by mattr03 in "Sharing AI progress in mathematics"

mattr03 — Tue, 06 Oct 2026 22:52:06 +0000

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.

New comment by mattr03 in "OpenAI’s Navier-Stokes release included a Lean 4 formal proof"

mattr03 — Thu, 10 Sep 2026 23:35:40 +0000

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

New comment by mattr03 in "Stockfish 19"

mattr03 — Thu, 10 Sep 2026 09:33:44 +0000

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