Yet another Hacker News

55 points matt_d 1 day ago 15 comments

s_Hogg 1 hour ago | parent

As someone who doesn't quite get all this, isn't the proposal here just checkers all the way down?

measurablefunc 34 minutes ago | parent

The proposal is that multiple checkers are unlikely to all have the same bugs so the more kernels you can use to check the results the more likely it is that the proof/code is consistent & correct (modulo set theoretic assumptions necessary for the correctness of the kernel).

nickysielicki 55 minutes ago | parent

Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

In other words, how much of the developments this year are directly attributable to LLMs using lean, versus lean just being a significantly more productive language for some subset of mathematics compared to English and LaTeX?

Given how much we’ve seen formalized this year it feels hard to believe that this couldn’t have happened earlier.

Follow up question: do you think mathematicians would be as upset about the rapid changes in their field if they were the result of a collective shared effort on github, authored entirely by humans who all share the credit, versus that same outcome but authored by a large language model?

In other words, are the mathematicians upset about large language models, or are they really just upset that formalization and massive collaboration have turned out to be highly effective and has negated the heroic angle that mathematicians previously enjoyed, thinking in a locked room by themselves?

Food for thought.

A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read, on par with C and Python, and I think it’s pretty hard to disagree with that. Next generations of models are going to be RL’d on Lean more and more because it pays dividends in winning the math war against their competitors, and this will benefit users of lean not only for mathematics but also as a general programming language and as a vehicle for other DSLs. For example, I think Sparkle (a Lean based HDL) or something like it makes a lot of sense in 2026 and beyond.

https://github.com/Verilean/sparkle

anonymous908213 40 minutes ago | parent

This is my hypothesis too. I work with LLMs daily. I use frontier models all the time, and I work in a startup that trains its own special-purpose models. At no point in the course of my work do I see anything resembling superhuman intelligence. I see superhuman stupidity, ie. stupidity so extreme that it exceeds what any human is capable of by orders of magnitude. So where are the superhuman math results coming from? Simple: translation. I've already thought this for a long time, that math is an obsfucated field and that programming already makes it far simpler to understand. So you train a machine to throw tons of compute at translating math into programming, and blow the field out of the water because it's effectively been deobfuscated. Math proofs had a sort of security by obscurity; they were not genuinely supremely difficult, but rather very few people worldwide worked on them and their work was heavily obscured, so the great deobfuscation machine comes along and trivialises that aspect and suddenly the facade crumbles. I think all of this could have been achieved a long time ago had humans done the deobfuscation, but there wasn't sufficient programming <--> maths cross-domain expertise or financial incentive to develop it.

AxEy 32 minutes ago | parent

> Suppose lean in its current state existed 15 years ago, and suppose the math community eagerly started contributing en masse to a shared repository of code. How much of the breakthroughs and longstanding questions in mathematics that we’ve seen answered this year do you think we would have solved?

(Former grad student in math here who has spent whole weeks formalizing in Lean lemmas that would be considered by professional mathematicians writing a mathematics text / paper as obvious ("without loss of generality we can assume that....", "it should be clear that...")

Probably very few or none.

These systems (mostly) don't help you discover new mathematics. They are a tool for formalization.

It just turns out that combining them with LLMs is the secret sauce. LLMs have quite a bit of creativity but make a lot of mistakes. The Lean typechecker never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.

nickysielicki 28 minutes ago | parent

Is that because you were starting from scratch and working alone, though?

Imagine a hypothetical project at the scale of the Linux kernel, with thousands of mathematicians building up organized and well-commented code, standing on each others shoulders.

anonymous908213 27 minutes ago | parent

Make a trivial adjustment to your final proposition and it would still hold, no?

> Humans have quite a bit of creativity but make a lot of mistakes. The Lean typecheck never makes a mistake but has no creativity. Get them to work together in an iterative loop and you get what we have now.

AxEy 18 minutes ago | parent

The speed matters massively. Also it seems that LLMs are... getting to be quite creative.

The point is that the there has to be an idea to try to check. Lean does not give you that.

xiaoyu2006 11 minutes ago | parent

I am a math undergrad and I tried lean. It probably is because of habit and familiarity but I still find lean proofs harder to read than NL proofs. I wonder what if the math education switch entirely to a formal language (not necessarily Lean) will be?

sigmar 27 minutes ago | parent

I don't understand what you're saying. Writing lean doesn't make it easier to formulate a proof. These LLMs are writing natural language proofs then formalizing after the NL proof is done. If humans were theorizing and exploring open problems in lean for the last 15 years, we'd be moving much slower than we have been with natural language.

xiaoyu2006 13 minutes ago | parent

Funnily NL is indeed different from formal language and does different in a way that makes a difference: https://www.scientificamerican.com/article/openais-blockbust...

alphabeta3r56 20 minutes ago | parent

I mean we had Coq for the longest time.

aureianimus 6 minutes ago | parent

I concur with one of the other replies: very few or none.

This is putting the cart before the horse: Progress in verification has been huge because of LLMs. Mathlib PRs spiked at the release of Opus 4.6, any of the big formalizations would not have been here without LLMs.

More surprising to me, OpenAI claims they're doing informal reasoning and only after do the formalization. This seems to match the way in which they release things. Of course they will have Lean in the training data, but I think this supports the mirror hypothesis: We'd have the same progress in mathematics if proof assistants didn't exist, it would just be a pain to verify correctness.

Fully agree on the potential for Lean as a generic programming language.

sinuhe69 27 minutes ago | parent

What does “verified” mean here? Someone has formalized verified the kernels or just different kernels cross check each others?