“Why not just use Lean?”

https://lawrencecpaulson.github.io//2026/04/23/Why_not_Lean.html

by ibobev • 3 months ago

304 209 3 months ago

lawrencecpaulson.github.io

MarkusQ2• 3 months ago

We need more of this.

For every "well of course, just...X, that's what everybody does" group-think argument there's a cogent case to be made for at least considering the alternatives. Even if you ultimately reject the alternatives and go with the crowd, you will be better off knowing the landscape.

sdenton4• 3 months ago

It depends!

Every time you go off the beaten path, you're locking yourself into less documentation, more bugs (since there's less exploration of the dark corners), and fewer people you can go to for help. If you've got 20+ choices to make, picking the standard option is the right choice on average, so you can just do it and move on. You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem.

The exceptions to this are when a) it becomes apparent that the standard tool doesn't actually fit your use case, or b) the standard tool significantly overlaps the core problem you're trying to solve.

c-linkage• 3 months ago

Which shows the lie of the common engineering trope "use the right tool for the job."

It really should be "use the same tool that everyone else is using so you don't have decide which tool is the right one -- the herd made that decision for you!"

MarkusQ2• 3 months ago

You have finite attention, so doing a research report on every dependency means you're never actually working on the core problem.

Reading that took five minutes and gave a good intro to the counter argument to Curry-Howard-all-the-things monomania. If having invested those five minutes, Lean still seems like the way to go (for whatever reason) fine. You are making a (closer to) informed choice, and likely better off than if you'd spent those five minutes doubling down on the conventional solution.

Most deviations from the group consensus are mistakes, but all progress comes from seeing past the group consensus. So making frequent small bets on peeking around your blinders is a good strategy.

lmm4• 3 months ago

Completely disagree; IMO we build far too many frameworks and alternatives (probably because it's fun) instead of a) enhancing the things that already exists to have the thing we want or b) just getting on with the actual work. The whole field would be much better off if we had half as many languages, half as many libraries, half as many build tools...

zermelo44• 3 months ago

Good post! +1

kccqzy3• 3 months ago

For the HN crowd who are generally programmers but not necessarily mathematicians, it’s more relevant to consider the programming side of things. There is a very good book (one I haven’t finished unfortunately) that covers Lean from a functional programming perspective rather than proving mathematics perspective: https://leanprover.github.io/functional_programming_in_lean/

I am learning Lean myself so forgive me as I have an overly rosy picture of it as a beginner. My current goal is to write and prove the kind of code normal programmers would write, such as real-world compression/decompression algorithms as in the recent lean-zip example: https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

readthenotes1• 3 months ago

I recall an experiment in proving software correct from the 1990s that found more errors in the final proof annotations than in the software it had proved correct.

Then, I foresee 2 other obstacles, 1 of which may disappear:

1. Actually knowing what the software is supposed to do is hard. Understanding what the users actually want to do and what the customers are paying to do --which aren't necessarily the same thing--is complex

2. The quality of the work of many software developers is abysmal and I don't know why they would be better at a truth language than they are at Java or some other language.

Objection 2 may disappear to be replaced with AI systems with the attention to do what needs to be done. So perhaps things will change in that to make it worthwhile...

jsmorph2• 3 months ago

Re 1: Discussing and guiding the desirable theorems for general-purpose programs has been a major challenge for us. Proofs for their own sake (bad?) vs glorious general results (good but hard?). Actual human guidance there can be critical there at least for now.

cayley_graph• 3 months ago

Mind linking the experiment? Sounds interesting.

Groxx2• 3 months ago

I think the hope for 2 is that those programmers would be forced into inaction by the language safety, rather than being allowed to cause problems.

I don't really think that works either, because there's endless ways to add complication even if you can't worsen behavior (assuming that's even possible). At best they might be caught eventually... but anyone who has worked in a large tech company knows at least a few people who are somehow still employed years later, despite constant ineptitude. Play The Game well enough and it's probably always possible.

deterministic• 3 months ago

Check out SeL4 (a proven correct micro kernel used by billions of devices worldwide) and CompCert (a proven correct C compiler used by Airbus).

dharmatech• 3 months ago

While reading though this book, I messed around with a basic computer algebra simplifier in Lean:

https://github.com/dharmatech/symbolism.lean

It's a port of code from C#.

Lean is astonishingly expressive.

NooneAtAll3• 3 months ago

what about non-functional programming?

FP is just as irrelevant for most programmers as the math you already shoved aside

DauntingPear7• 3 months ago

Hmm like the “new” JS Fetch api with `then` chaining? What about map, filter, reduce? Anonymous functions? List comprehensions? FP is everywhere. Pure FP code isn’t seen very often, as side effects are necessary for most classes of programs, but neither is pure OOP code, as not everything is dynamically dispatched, nor imperative code, as Objects or functions may more cleanly describe/convey something in code.

threethirtytwo• 3 months ago

FP and math are the same concept.

The semantics of math are equation based.

Everything in the math universal language is defined as an expression or formula.

All proofs are based on this concept.

To translate this into programming think about what programming is? Programming rather being a single line formula is a series of procedures.

  1. add 1
  2. add 3
  3. repeat.

in functional programming you get rid of that and you think from the perspective of how much of a program can you fit into a single one liner? An expression? Think map, reduce, list comprehensions, etc.

That is essentially what functional programming is. Fitting your entire program onto one line OR fitting it into a math expression.

The reason why you see multiple lines in FP languages is because of aliasing.

  m = b + c
  y = x + m

is really:

  y = x + (b + c)

This is also isomorphic to the concept of immutability. By making things immutable your just aliasing part of the one liner...

So functional programming, one line programs, formulas and equations in math, and immutability are essentially ALL the same concept.

That is why lean is functional. Because it's math.

kccqzy3• 3 months ago

I shoved math aside because I think for most of the HN crowd it wouldn’t be a good use of their time to do what mainstream mathematics is about, like the “things such as Grothendieck schemes and perfectoid spaces” the article also references. FP is much more relevant because for any program for which a proof of correctness is worthwhile, you can always extract a functional core of that program (functional core, imperative shell). And that functional core will be easier to prove than if it were written in an imperative style.

icosahedron2• 3 months ago

You might like looking at Dafny. It is more imperative focus, but has many of the same software proving functionality that Lean has.

It is different in that it uses SMT instead of dependent types and tactics to prove the software, but I found it more approachable.

Also, it compiles to several target languages, whereas Lean 4 only compiles to C and therefore only supports the C ABI.

grogers• 3 months ago

Have you tried dafny, which seems roughly comparable for your purposes? I heard some buzz about it a little while ago but I haven't been following this space closely.

nextos• 3 months ago

Dafny and F*, which competes directly with Lean but is more guided towards SWE, are definitely worthy of consideration.

smj-edison9• 3 months ago

I think what's interesting about Lean is that Lean is a language, and what most people are talking about is a library called Mathlib. From what I've read about Mathlib, the creators are very pragmatic, which is why they encode classical logic in Lean types, with only a bit of intuitionistic logic[1].

[1] for those unfamiliar with math lingo, classical logic has a lot of powerful features. One of those is the law of the excluded middle, which says something can't be true and false at the same time. That means not not true is true, which you can't say in intuitionistic logic. Another feature is proof by contradiction, where you can prove something by showing that the alternative is unsound. There's quite a few results that depend on these techniques, so trying to do everything in intuitionistic logic has run into a lot of roadblocks.

bowsamic2• 3 months ago

This makes it good for formal maths, but bad for philosophy, since it means it can’t encode the speculative movement

drdeca2• 3 months ago

Which logic are you saying “can’t encode the speculative moment”?

I think the two logics can emulate one another? Or, at the very least, can describe what the other concludes. I know intuitionistic logic can have classical logic embedded in it through some sort of “put double negation on everything”. I think if you add some sort of modal operator to classical logic you could probably emulate intuitionistic logic in a similar way?

vscode-rest• 3 months ago

When/why would one prefer to use intuitive logic, given the limitations/roadblocks?

thaumasiotes6• 3 months ago

For ideological reasons.

ux2664786• 3 months ago

Classical logic has plenty of limitations/roadblocks, all logics do. Logic isn't a unified domain, but an infinite beach of structural shards, each providing a unique lens of study.

Classical logic was rejected in computer science because the non-constructive nature made it inappropriate for an ostensibly constructive domain. Theoretical mathematics has plenty of uses to prove existences and then do nothing with the relevant object. A computer, generally, is more interested in performing operations over objects, which requires more than proving the object exists. Additionally, while you can implement evaluation of classical logic with a machine, it's extremely unwieldy and inefficient, and allows for a level of non-rigor that proves to be a massive footgun.

smj-edison9• 3 months ago

As far as I understand it, classical mathematics is non-constructive. This means there are quite a few proofs that show that some value exists, but not what that value is. And in mathematics, a proof often depends on the existence of some value (you can't do an operation on nothing).

The thing is it can be quite useful to always know what a value is, and there's some cool things you can do when you know how to get a value (such as create an algorithm to get said value). I'm still learning this stuff myself, but inuitionistic logic gets you a lot of interesting properties.

gowld2• 3 months ago

Excluded-middle `true` means "[provable] OR [impossible to disprove]".

Intuitionist/Constructivist `true` means, "provable".

The question you are asking determines what answers are acceptable.

Why build an airplane, if you already know it must be possible?

amavect5• 3 months ago

In constructive logic, a proof of "A or B" consists of a pair (T,P). If T equals 0, then P proves A. If T equals 1, then P proves B. This directly corresponds to tagged union data types in programming. A "Float or Int" consists of a pair (Tag, Union). If Tag equals 0, then Union stores a Float. If Tag equals 1, then Union stores an Int.

In classical logic, a proof of "A or not A" requires nothing, a proof out of thin air.

Obviously, we want to stick with useful data structures, so we use constructive logic for programming.

ogogmad• 3 months ago

There are non-computational interpretations of intuitionistic logic too, like every single thing mentioned on this page: https://ncatlab.org/nlab/show/synthetic+mathematics

I think stuff like "synthetic topology", "synthetic differential geometry", "synthetic computability theory", "synthetic algebraic geometry" are the most promising applications at the moment.

It can also find commonalities between different abstract areas of maths, since there are a lot of exotic interpretations of intuitionistic logic, and doing mathematics within intuitionistic logic allows one to prove results which are true in all these interpretations simultaneously.

I'm not sure if intuitionism has a "killer app" yet, but you could say the same about every piece of theory ever, at least over its initial period of development. I think the broad lesson is that the rules of logic are a "coordinate system" for doing mathematics, and changing the rules of logic is like changing to a different coordinate system, which might make certain things easier. In some areas of maths, like modern Algebraic Geometry, the standard rules of logic might be why the area is borderline impenetrable.

seanhunter5• 3 months ago

It’s not intuitive, it’s intuitionist. I’m not saying that to nitpick it’s just important to make the distinction in this case because it really isn’t intuitive at all in the usual sense.

Why you would use it is it’s an alternative axiomatic framework so you get different results. The analogy is in geometry if you exclude the parallel postulate but use all of the other axioms from Euclid you get hyperbolic geometry. It’s a different geometry and is a worthy subject of study. One isn’t right and the other wrong, although people get very het up about intuitionism and other alternative axiomatic frameworks in mathematics like constructivism and finitism.

ngruhn• 3 months ago

You're walking down a corridor. After hours and hours you ask "is it possible to figure how far it is to the nearest exit?". Your classical logic friend answers: "Yes, either there is no exit then the answer is infinity. Or there is an exit then we just have to keep walking until we find it. QED"

This kind of wElL AcTUaLly argument is not allowed in constructive logic.

Twey• 3 months ago

Intuitionistic logic is a refinement of classical logic, not a limitation: for every proposition you can prove in classical logic there is at least one equivalent proposition in intuitionistic logic. But when your use of LEM is tracked by the logic (in intuitionistic logic a proof by LEM can only prove ¬¬A, not A, which are not equivalent) it's a constant temptation to try to produce a constructive proof that lets you erase the sin marker.

In compsci that's actually sometimes relevant, because the programs you can extract from a ¬¬A are not the same programs you can extract from an A.

zodiac• 3 months ago

We still care about computation and algorithms even when proving theorems in a classical setting!

For e.g., imagine I'm trying to prove the theorem "x divides 6 => x != 5". Of course, one way would be to develop some general lemma about non-divisibility, but a different hacky way might be to say "if x divides 6 then x ∈ {1, 2, 3, 6}, split into 4 cases, check that x != 5 holds in all cases". That first step requires an algorithm to go from a given number to its list of divisors, not just an existence proof that such a finite list exists.

Chinjut• 3 months ago

You mean intuitionistic logic, not "intuitive logic".

smj-edison9• 3 months ago

Oops, just edited. I'm still fairly new to this area, so I keep mixing up my terms :)

thaumasiotes6• 3 months ago

Another feature is proof by contradiction, where you can prove something by showing that the alternative is unsound.

As far as lean is concerned, this isn't an example of classical logic. It's just the definition of "not" - to say that some proposition implies a contradiction, and to say that that proposition is untrue, are the same statement.

Most "something"s that you'd want to prove this way will require a step from classical logic, but not all of them. (¬p ⟶ F) ⟶ p is classical; (p ⟶ F) ⟶ ¬p is constructive.

smj-edison9• 3 months ago

So proof by contradiction proves ¬p, but it requires the law of excluded middle to prove p (in the case of ¬p -> F)? I didn't realize that was constructive in the first case.

zozbot23422• 3 months ago

More generally, any negative statements can be proven classically, even in intuitionistic logic. Intuitionistic logic does not have the De Morgan duality found in classical logic, you have to go to linear logic if you want to recover that while keeping constructivity. (The "negative" in linear logic actually models requesting some object, which is dual to constructing it. The connection with the usual meaning of "negative" in logic involves a similar duality between "proposing" a proof and "challenging" it.)

cubefox• 3 months ago

One of those is the law of the excluded middle, which says something can't be true and false at the same time.

That would be the law of non-contradiction (LNC). The law of the excluded middle (LEM) says that for every proposition it is true or its negation is true.

LEM: For all p, p or not p.

LNC: For all p, not (p and not p).

Classical logic satisfies both, intuitionistic logic only satisfies LNC.

zozbot23422• 3 months ago

I think what's interesting about Lean is that Lean is a language, and what most people are talking about is a library called Mathlib. From what I've read about Mathlib, the creators are very pragmatic, which is why they encode classical logic in Lean types, with only a bit of intuitionistic logic

The computer science folks are now working on their own CSLib. https://www.cslib.io https://www.github.com/leanprover/cslib Given that intuitionistic logic is really only relevant to computational content (the whole point of it is to be able to turn a mathematical argument into a construction that could in some sense be computed with), it will be interesting to see how they deal with the issue. Note that if you write algorithms in Lean, you are already limited to some kind of construction, and perhaps that's all the logic you need for that purpose.

hackandthink• 3 months ago

the law of the excluded middle, which says something can't be true and false at the same time

This is the not excluded middle, it is the "Law of noncontradiction"

Excluded middle means: either p is true or the negation of p is true

https://en.wikipedia.org/wiki/Law_of_noncontradiction

leonidasrup• 3 months ago

Five stages of accepting constructive mathematics:

Denial

Anger

Bargaining

Depression

Acceptance

A talk about constructive mathematics by Andrej Bauer at the Institute for Advanced Study.

https://www.youtube.com/watch?v=21qPOReu4FI

http://dx.doi.org/10.1090/bull/1556

groundzeros20157• 3 months ago

Type theory and lean is more interesting to people who like computers than to people who like math.

baq• 3 months ago

citation needed, Tao certainly is on record using Lean and that carries some weight.

also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.

groundzeros20157• 3 months ago

The link is exactly what I’m saying. I only hear cs people talk about it.

For mathematicians a proof is a means to an end, or a medium of expression - they care about what they say and why.

The correspondence isn’t about C programs corresponding to proofs in math papers. It’s a very a specific claim about kinds of formal systems which don’t resemble how math or programming is done.

soulofmischief• 3 months ago

Terence Tao, one of the most important living mathematicians, specifically embraces Lean and has been helping the community embrace it.

What you've done here is an overgeneralization. "People who like math" and "people who like computers" are massive demographics with considerable overlap.

groundzeros20157• 3 months ago

one of the most important living

Maybe. But more clearly one of the most popular online.

vitriol83• 3 months ago

Formalised proofs and Lean in particular are still too cumbersome for the ``working'' mathematician to use it day-to-day for research-level math. But clearly there is some interest on where it may take us in future.

ux2664786• 3 months ago

The set theorists decided that mathematics is the overarching superdomain over all study of structure. You don't get to pick and choose. Either mathematics is a suburb of logic and these two things are separate, or they're not and ZFC dogmatics need to accept they don't have a monopoly on math.

I of course fully support reinstating logicism, but the same dogmatics love putting up a fight over that as well.

groundzeros20157• 3 months ago

Mathematicians use logic to talk about the mathematical world. But logic is not the world.

smj-edison9• 3 months ago

I think the most surprising thing I've learned taking formal math in college is just how much mathematicians are pragmatists (at least for my teacher with sample size n=1). They're much more interested in new ways to think about ideas, with a side effect of proofs for correctness. The proof is more about explaining why something works, not that it does.

I'm going to take a formal logic class in the fall, and my professor said something akin to "definitely take it if you're interested, just be aware that it probably won't come in use in most of the mathematics done today." The thing is the foundations are mostly laid, and people are interested in using said foundations for interesting things, not for constantly revisiting the foundations.

I think this is one reason most mathematicians don't see a need for formal proof assistants, since from their perspective it's one very small part of math, and not the interesting one.

This is not to say that proof assistants are a dead end—I find them fascinating and hope they continue to grow—but there's a reason that they haven't had a ton of traction.

kccqzy3• 3 months ago

I would’ve expected that people who like computers will converge around something like Idris. It’s marketed as a development tool, not a tool for formalizing mathematics even though it could be used as a proof assistant.

jsmorph2• 3 months ago

Slightly off topic: This project https://agentcourt.ai/arb/analysis/index.html uses a Go/Lean hybrid design. The Go code is mostly glue, and the Lean code is the logic https://github.com/agentcourt/adjudication/tree/main/arb/eng.... It's not math-intensive. Really just functional programming with some interesting proofs (including soundness ideally). Go code can migrate to Lean code when that makes sense.

c0balt3• 3 months ago

Isabelle/HOL as a language is nice, but the tooling has deep flaws even outside the pure desktop-first app approach.

The language is different (not necessarily better) in comparison to Lean, but I do agree with some of the points on dependent types. It seems both languages mostly just made different tradeoffs, which imo, were fair and have shaped them into quite efficient tools for their domains. The domain of "proofs" is large and different paradigms just have different strengths/weaknesses, Lean just specialized for a different part of this space.

Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean. It might also be nice to use for explorative phases but is a resource hog, it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer".

Working on Isabelle itself however is painful (especially communicating with developers) in comparison to Lean. Things like "we don't have bugs just unexpected behaviour" on the mailing list just seems childish/unprofessional. The callout to RAM consumption of Lean and related systems is also a bit of joke when looking at Isabelle's gluttony for RAM.

zozbot23422• 3 months ago

but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer".

One issue with this is that coming up with a quickly-checkable certificate for UNSAT is not exactly a trivial problem. It's effectively the same as writing a formal proof.

vintermann• 3 months ago

Last I checked, Isabelle/HOL used a custom Emacs mode as their interface. (I could be mixing it up with one of the other HOLs).

c0balt3• 3 months ago

The current GUI interface is Isabelle/jedit. Afaik, no Emacs interface is officially provided atm.

thaumasiotes6• 3 months ago

Sledgehammer is nice but probably just a question of time until an equivalent can be ported/created for Lean.

I have no knowledge of what sledgehammer is. However...

it also makes proofs concise but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer"

This description makes sledgehammer sound identical to Mathlib's `grind`. https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

c0balt3• 3 months ago

The goal (ATP) is similar but the idea is a bit different, sledgehammer is not directly learning/applying rules but instead effectively a driver for invoking a bunch of ATPs + SMT solvers at once on a goal in Isabelle/HOL.

You can read more about it here: https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf

gorgoiler• 3 months ago

It’s been decades since I could claim to know anything about this field so I’m probably completely wrong in how I read this, but the idea that one might build a theorem prover (“ML!”) for one’s non-ML programming language and have the prover itself accidentally be a really good general purpose programming language … is very funny.

hutao• 3 months ago

To clarify: ML started out as a scripting language for Robin Milner's proof assistant, LCF. The formal system, or "logic," is implemented in a minimal, trusted kernel, and the proof data structure is protected as an abstract data type that can only be constructed through the trusted kernel. On top of the kernel, tactic scripts may be defined to manipulate proof objects and facilitate proof search/automation.

Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).

nrds5• 3 months ago

The author appears to have a serious misconception about Lean, which is surprising since he seems to be quite knowledgeable in the area.

Specifically, the author seems to be under the impression that Lean retains proof objects and the final proof to be checked is one massive proof object, with all definitions unfolded: "these massive terms are unnecessary, but are kept anyway" (TFA). This couldn't be further from the truth. Lean implements exactly the same optimization as the author cherishes in LCF; metaphorically, that "The steps of a proof would be performed but not recorded, like a mathematics lecturer using a small blackboard who rubs out earlier parts of proofs to make space for later ones" (quoted by blog post linked from TFA). Once a `theorem` (as opposed to a `def`) is written in Lean4, then the proof object is no longer used. This is not merely an optimization but a critical part of the language: theorems are opaque. If the proof term is not discarded (and I'm not sure it isn't), then this is only for the sake of user observability in the interactive mode; the kernel does not and cannot care what the proof object was.

burakemir• 3 months ago

A proof object in dependent type theory is just the term that inhabits a type. So are you saying the Lean implementation can construct proofs without constructing such a term?

nrds5• 3 months ago

No, I'm saying it is checked and then discarded. (Or at least, discarded by the kernel. Presumably it ends up somewhere in the frontend's tactic cache.) That matches perfectly the metaphor, "rubs out earlier parts of proofs to make space for later ones".

The shared misconception seems to be in believing that because _conceptually_ the theory implemented by Lean builds up a massive proof term, that _operationally_ the Lean kernel must also be doing that. This does not follow. (Even the concept is not quite right since Lean4 is not perfectly referentially transparent in the presence of quotients.)

vilhelm_s• 3 months ago

Yeah. I guess the abstract type approach saves some memory, but it's a constant factor thing, not an asymptotic improvement. The comment that Lean wastes "tens of megabytes" seems telling: it seems like something that would be a critical advantage in the 1980s and 1990s, when Paulson first fought these battles, but maybe less important today...

nrds5• 3 months ago

To be fair, lean wastes and leaks memory like a sieve, but this is almost all in the frontend. It has nothing to do with the kernel or the theorem proving approach chosen.

auggierose2• 3 months ago

It is more a conceptual thing. In LCF, proofs and terms are different things, and that is how it should be in my opinion. This Curry-Howard confusion is unnecessary, but many people don't realise that, they think it is the only way to do math on a computer. You can still store proofs in LCF if you want, and use them; just as in Lean, you might be able to optimise them away.

nrds5• 3 months ago

You have done no more to show an actual distinction in the approach than TFA and its linked blog post... It sounds like a naming thing to me. On one side we name the term/program as a term and see it as something checked by the kernel, and on the other you name the term/program as a program and see it as something executed by the runtime. What's the difference?

rzerowan• 3 months ago

One of those names that forces a double take when seen disconnected from context:

'Lean or purple drank is a polysubstance drink used as a recreational drug. It is prepared by mixing prescription-grade cough or cold syrup containing an opioid drug '

proving that one of the hardest problem in CS - 'naming things' still keeps on keeping on.

bradleyy2• 3 months ago

The two hardest problems in CS: * naming * cache invalidation * off by one errors

InkCanon• 3 months ago

Wait till you hear what Rocq was originally called!

heliumtera• 3 months ago

The recommended way to install Lean is through VS Code

Is that enough reason?

EFreethought• 3 months ago

Yes.

I am tired of my time in tech being just using MS products that all depend on each other.

loglog• 3 months ago

"I believe that almost anything that has been formalised today in any system could have been formalised in AUTOMATH. Its main drawbacks were its notation, which really was horrible, and its complete lack of automation. Proofs were long and unreadable." That's like saying that anything that could be programmed today in your modern language of choice could have been programmed 50 years ago in assembly. Technically yes, economically no.

strbean• 3 months ago

Well, assembly languages are generally Turing complete. Not sure what the parallel would be in proof engines.

pstoll• 3 months ago

Feels like all the write ups that point out the short comings of eg Python for scientific computing.

Sure, except that once you have a community at critical mass around a reasonably good tool, that trumps most other things. Momentum builds. People write tutorials, explainers, better documentation, etc. it hits escape velocity.

Feels like Lean, with Terrance Tao as a strong proponent / cheerleader, is in that space.

Everyone who argues “but language X is better” … may not be wrong, but they are not making the argument that matters. Is it better than the thing everyone else knows and can use and has more people hours going into it to improve it?

Feels like a “worse is better” situation; or maybe “good and popular is good enough”.

ModernMech3• 3 months ago

once you have a community at critical mass around a reasonably good tool, that trumps most other things

This matters a lot less in the age of AI. AI doesn't need a massive number of community-built libraries, it can just write its own. It doesn't need a million tutorials floating out there on the interwebs because unlike most programmers, it will actually read the spec and documentation (tutorials are just projections of the docs/spec anyway). AI doesn't have to avoid languages with no job market because it just needs to do the job at hand, not build a career. This makes it easier for small languages and DSLs to gain usage where they never would have before.

I think AI might spell the end of the language monoculture (top 20 are mostly slight variations on languages circling the same design) that has persisted in programming.

tehjoker• 3 months ago

It's the opposite and has been recognized for years. AI depends on training data and this nearly freezes the use of languages that were popular at the time of inception. Hopefully that is not true.

AI needs community libraries if there is to be interoperability and baseline quality between systems. At least at this level of quality and development.

pfdietz• 3 months ago

I think the point that LLMs should enable effective translation between different formalisms is a good one. So I don't see the choice as being a big issue. This is especially the case here because to a large extent the translations can be checked automatically.

danilafe7• 3 months ago

People tell me Lean is really good for functional programming. However, coming from Agda, it feels like a pretty clunky downgrade. They also tell me it's good for tactics, but I've found Coq's tactics more powerful and ergonomic. Maybe these are all baby-duck perceptions. So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.

moomin2• 3 months ago

Thing is, it comes after both. Maybe it is just being a jack of all trades, but something made it success when the others remain fairly niche.

portly• 3 months ago

When I woke up this morning I could not have predicted someone calling a proof assistant a "Jack of all trades"

capitalhilbilly• 3 months ago

I think its pretty clear that being too early has been as bad as being too late for most technologies. There are a few that have gradually gained community after decades but it is easier to make a poor copy of one of them and have better momentum and less skepticism.

btilly2• 3 months ago

In other words, it is a network effect.

My perspective is that network effects are far less long-lasting than they feel in the moment. For example if being decent at everything and having a huge community was the only thing that mattered, Perl would still be a big deal. Many similar examples exist.

In the case of Lean, being the first with a huge library really makes a difference. Just as Perl got a big boost from having CPAN. (Which was an imitation of CTAN, except for a programming language instead of TeX.)

But, based on scaling laws, we should expect the value of a large library for most users to grow around the log of the size of the library. (See https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do... for the relevant scaling laws.)

When your library is small, this looks like an insurmountable barrier. But you don't have to match the scale for factors of usability to become more important. And porting mathematical libraries is a good target for LLMs. The source is verified, the target is verifiable, and the reasoning path generally ports.

The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect. Because if their library can be ported to your platform, then your proof can probably be ported to their platform as well!

danilafe7• 3 months ago

The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect

This is a nice thought, but with Agda in particular it's just not true. It's one of the few languages I've seen that's sufficiently unrepresented in training data. Frontier LLMs (Codex, Claude Code) reliably say "I realized I can't do this." after wasting lots of tokens going back and forth.

In fact, I think this positions Agda uniquely poorly.

gucci-on-fleek• 3 months ago

except for a programming language instead of TeX

TeX is a programming language. It's not a very good programming language, but people have implemented floating-point math [0], regular expressions [1], an Arduino emulator [2], and terminal input/output [3] in pure TeX. The last two examples are obscure, but the first two examples are used (internally) by the vast majority of modern LaTeX documents.

[0] https://github.com/latex3/latex3/blob/develop/l3kernel/l3fp....

[1] https://github.com/latex3/latex3/blob/develop/l3kernel/l3reg...

[2] https://www.ctan.org/pkg/avremu

[3] https://www.ctan.org/pkg/reverxii

ModernMech3• 3 months ago

fyi it's Rocq now: https://en.wikipedia.org/wiki/Rocq

markusde2• 3 months ago

I'm curious what you like about Agda functional programming? Many of the praises I hear about it have to do with it's dependent pattern matching, and I think Lean suffers a lot more in that regard. I'm curious though if you still find Agda friendlier for "normal" fp (and if so, how?)

danilafe7• 3 months ago

Its parameterized modules, extremely elegant yet flexible mixfix notation mechanism, the various niceties around pattern matching (though this one might be a bit of Stockholm syndrome; Agda doesn't nicely allow pattern matching anywhere except at function clauses), the fact that records, GADTS, and modules all feel like aspects of the same thing, and the fact that typeclasses are 'just' records that are automatically filled in. The typeclass and module features IMO already give it some edge over Haskell. I don't know if it's friendlier, but it is more ergonomic.

floxy• 3 months ago

Thoughts on Idris?

wk_end• 3 months ago

Idris feels mostly dead to me at this point. Which breaks my heart, because for a split second it had real momentum around it.

Not OP, but as Haskell-derived dependently-typed languages Idris and Agda are quite similar, so I suspect if they like one they’d like the other.

JuniperMesos2• 3 months ago

I've used agda a tiny bit and Lean somewhat more, and I definitely found it much easier to write functional programs not focused on mathematical proofs in Lean than Agda. IIRC the difference was mostly tooling - Agda's documentation is kind of bad and it's a pain to get it working on your system (and it really wants you to be using Emacs specifically). Whereas Lean documents how to write the cat utility in its own docs and generally has a much better, more modern tooling experience.

danilafe7• 3 months ago

I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + tooling combination). Agda worked out of the box with macOS homebrew. Agda's docs are petty bad, but I've found its cross-linked module documentation incredibly useful. The main issue is knowing something exists.

solomonb3• 3 months ago

I prefer agda as proof checker but its not a practical choice for building software. Lean feels like it could legitimately become a successor to Haskell as the go to functional programming language for software development.

danilafe7• 3 months ago

I think what holds Agda back from being "practical" is that it just doesn't have good tactics. You can't easily automate proofs and even simplification techniques require some language-level tricks[1]. There's technically support for elaborator reflection (as in Idris) but it's painful and impossible to debug. Certainly nowhere near where Coq and Lean are.

[1]: like this one I've used for several proofs so far: https://danilafe.com/blog/agda_expr_pattern/

lmm4• 3 months ago

So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.

To me that feels like a community that's finally matured enough to start getting on with things. Perfect tools aren't the point; get tools that are good enough and do actual work with them.

antonvs• 3 months ago

Sounds like an excuse for mediocrity.

You can apply that same argument for the of Python in the ML world. It results in all sorts of pain points that everyone has to deal with all the time.

ibobev2• 3 months ago

What about the performance characteristics of the Lean programs? I know it is a natively compiled language, but is the code it produces comparable to that of modern system programming languages in terms of performance?

ted_dunning2• 3 months ago

Oddly enough, most uses of Lean never actually run the program. The fact that it type checks is enough to prove the theorem in question.

That said, if execution is seriously required for your problem along with strong logic on the side, you may prefer Dafny which transpiles the computation part of your proof to C++ or Go.

ibobev2• 3 months ago

But still, Lean is executable and can be used as an ordinary programming language.

WhitneyLand• 3 months ago

The most important thing is keeping up the momentum to formalize more proofs and continue to strengthen the libraries and foundational work.

If that momentum is strongest with Lean so be it. At the same time things become more machine verifiable, converting to a new system will also become easier. It can already be strongly assisted using a general agent like Claude Code.

ifh-hn3• 3 months ago

I keep seeing articles about Lean recently on HN. Never heard of it before. I'm not a mathematician and not a professional developer so my opinion might not mean shit, but I can't make head nor tail of it. I can't understand what half of what the website is talking about.

icosahedron2• 3 months ago

It's a paradigm shift, that's for sure.

I'm still in the throes of learning it myself, and it's quite the journey. I love the promises behind it, but I'm not yet far enough along to know if they are kept or if it's just kool aid (or perhaps purple drank?)

ifh-hn3• 3 months ago

I've never heard of purple drank before, not American. Which came first? The language or drug?

jojomodding2• 3 months ago

Its a software where you type your maths proofs in and a "yes" comes out. Except if your proof is broken, then a "no" comes out. Of course, sometimes the computer is just a bit dumb at intuiting the intermediate steps, so you need to explain like a 10-year-old child (or else you get a "no" as you failed to convince the computer). And storing all these explanations takes memory. And you have to speak the somewhat idiosyncratic language of the computer, which you can imagine a bit like LaTeX but more easily parseable and less ambiguous.

The blog article author is saying that Lean is like a younger child (that needs more intermediate steps explained), stores proofs more inefficiently (taking more memory) and that its computer proof language is harder to read for humans. Additionally there is a technical point about dependent types, which are the principle around which the computer proof language is organized (the same way a programming language might be organized around object-orientism).

ifh-hn3• 3 months ago

Thanks for taking the time to explain, rather than drive by downvote. It doesn't seem like this would be useful to me, or certainly I have no use for it that I can think of.

asdfman123• 3 months ago

I am going to build an alternative to Lean called Purple Drank

bradleyy2• 3 months ago

Do not be surprised when I fork and call it Sizzurp.

asparagui• 3 months ago

I was going to call my project that but Claude said that wasn't professional. rip "a delightful mixture of lean"

red-iron-pine• 3 months ago

ngl assumed this was about supply management or purple drank

Propositions as types is a duality linking the logical signs ∀ , ∃ , → , ∧ , ∨ with the type constructors Π , Σ , → , × , + . It is beautiful, fascinating and theoretically fruitful, but it is not the only game out there. I have seen “proof assistant”

raphlinus• 3 months ago

People interested in alternatives to Lean should also look at Metamath. It has nowhere near the adoption that Lean is getting, but is holding its own in [100] theorems results.

It has some advantages and compelling properties, not least of which is that it's very simple, so much so that there are many implementations of checkers; most other proof systems are ultimately defined by a single implementation. It's also astonishingly efficient — the entire database can be checked in less than a second. Set theory is also a familiar foundation for mathematicians, though the question of which is a better foundation compared with type theory is very controversial. Mario Carneiro pushed forward the development of Metamath in his thesis [0].

There are downsides also, including junk theorems, and automation is weaker. It's possible that types really help with the latter. Even so, I think it's worthy of study and understanding.

[0] https://digama0.github.io/mm0/thesis.pdf

[100] https://www.cs.ru.nl/~freek/100/

c7b• 3 months ago

Lean isn't the most loved proof assistant by mathematicians, it's not the most suited to formal verification of software, it just sort of works for both. Yet it's got the thing that's arguably the hardest to achieve, momentum. Compounded by the fact that in the AI age, the amount of publicly available human-written code directly affects how well agents can produce new code.

j2kun• 3 months ago

If you write an article shitting on a popular thing because it eclipses the popularity of your favorite thing (and essentially calling the people who use it ignorant sheep), chances are good you are part of a self-fulfilling prophecy, pushing people away from your community.

jojomodding2• 3 months ago

I do not get why not needing proof objects is desirable. It seems good to have a defined way to store proofs that has a very tight spec and can thus have competing implementations, like in https://arena.lean-lang.org/. The LCF approach couples the proof format to the module system of a programming language.

Occasionally, inspecting that proof term is useful to see what happened in a proof.

Then again, I also like dependent types.

zozbot23422• 3 months ago

You can use reflection in dependently-typed proof systems to avoid storing proof objects for expensive computations and replace them with a proof of a general algorithm instead (much like in the LCF approach: the general algorithm proof is the equivalent of a compiler checking that the module system use in a LCF tactic is sound).

BlanketLogic2• 3 months ago

I think the author is confkating two different things. There are technical problems with sticking to constructive purity when it comes to mathematics (setoid hell, avoiding excluded middle, real number formalization etc). Then there are social aspects. The community's 'cultist' ( his words) adherence to constructive logic. Saying this is the reason rocq lost out to lean seems wrong.

Firstly, there is value of the attempt. By staying true to constructive logic, there was a lot of progress (compcert verified c compiler, cubical agda etc).

Secondly, there were other confounding variables (tooling, network effects). Claiming rocq lost out to lean due to community's obsession is a bit of reductive argument.

But author is an expert. I will defer to him. His point about sledgehammer approach working well in the new AI world is very interesting though.

still_grokking• 3 months ago

Can someone ELI5 that for me?

Is this the mathematician's variant of "my language is better than your language", or what does this post actually discus? Something fundamental in the philosophy underpinning things or just the way to express them?

BlanketLogic2• 3 months ago

Paulson is a lead developer of Isabelle , a proof assistant that is not based on dependent types.

Is this the mathematician's variant of "my language is better than your language",

Almost. A closer analogy is comparing paradigms, say OOP vs functional programming.

Isabelle is different from the big three - rocq. lean and agda. The latter three have propositions as types. The type of your function is the theorem statement. The function body is the proof. Isabelle works differently. Author makes a convoluted argument that (a) one doesn't have to stick to the currently popular paradigm and (b) in conjunction with AI, Isabelle offers distinct benefits.

ianhorn2• 3 months ago

I remember trying to play around with Coq/Rocq and a few others about 15 years ago, and I couldn’t make heads or tails of them. Not the concepts, but the software. What’s weird about proof assistants/interactive provers is that the “interactive” part makes it a combo of IDE and language and they seem to get pretty tightly coupled in practice. You can’t talk about the language without talking about the environment you use it in.

I’m not the biggest VS code fan, but a battle honed extensible IDE used by zillions and maintained by $$$ has proved itself miles ahead of the environments for alternatives. As far as i can tell, the excellent onboarding path that is the Natural Numbers Game is possible because of VS code’s hackability and ecosystem.

My main concern as I’m learning lean is that the syntax extensibility seems to be a double edged sword. Once i’ve learned a language, i want to be able to read code written in it. If everything is in a project’s own DSL, that can get out of hand, but that comes down to community/ecosystem so i’m crossing my fingers.

bawolff• 3 months ago

I have been told that when proposing to formalise mathematics these days, you have to explain why you are not using Lean....Amidst the hype around today’s progress, we must remember how we got here. It was not by people following the crowd.

Im not a mathmatician, but in my experience if you are trying to do something novel, you should follow the crowd except for things that impact what you are trying to achieve. Otherwise you spend a lot of extra time sorting through issues on the part that doesn't matter which could be better spent on the novel part.

singularity2001• 3 months ago

Formal proofs are made to be done by AI.

If a green checkmark goes away so be it. AI might or may not understand how to fix it but it's no burden to the user / developer.

“Why not just use Lean?”

Related Stories