“Why not just use Lean?”
lawrencecpaulson.github.io
lawrencecpaulson.github.io
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...
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...
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.
Ah! That's funny :)
In practice there are always ways to circumvent safety, especially when it is easier than the alternative.
In a Typescript codebase I work on, I configured the type-checker to fordbid `any`. Should be easy enough to use `object` When we don't know the type, right? Well then things started being serialized into `string` way more often than I'd like...
the exception is if you explicitly state X is a true statement, as many have some kind of bypass like that (an axiom or assumption or whatever). you could build a system that uses this everywhere to break most of the rules, like you can use `any` everywhere, but it'll be extremely obvious if that's the case.
My point is: if you try to force people into inaction, chances are they will bypass you.
https://github.com/dharmatech/symbolism.lean
It's a port of code from C#.
Lean is astonishingly expressive.
FP is just as irrelevant for most programmers as the math you already shoved aside
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.
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
y = x + (b + c)
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.
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.
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.
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.)
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!
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.
I wonder how compiler technology would do. Possibly as a component of an attempted solution.
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...
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.
I don't understand the forced vscode path, just let me get it as normal software in a convenient way and run it as a tool
[1]: like this one I've used for several proofs so far: https://danilafe.com/blog/agda_expr_pattern/
While we're at it, another major concern for me is the inscrutability of Agda's error messages. I've had one error message single-handedly overflow my tmux scrollback buffer. There's no way I'm going to be able to interpret that.
lmao i've been there. Agda is my first choice for proof checker and for math-y explorations but its not gonna be a replacement for Haskell as a production programming language.
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.
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.
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.
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.
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...
You can read more about it here: https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf
Why isn't there a tactic in Lean to prove things by SMT using Z3? This could be integrated to grind
[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.
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?
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.
It's not that classical logic is useless, it's just that it's not particularly appropriate to choose as the basis for a system built on algorithms. This goes both ways. Set theory was taken as the foundation of arithmetic, et al. because type theory was simply too unwieldy for human beings scrawling algebras on blackboards.
So not sure it would be "unwieldy", it's a remarkably simple addition and it may avoid some of the pain points with sets? But again, not even a mathematician.
I don’t think that logic holds in mainstream mathematics (it will hold in constructive mathematics by definition, and may hold in slightly more powerful philosophies op mathematics) because there, we can prove the existence of many functions and numbers that aren’t computable.
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.
It's not as simple as that. Classical mathematics can talk about whether some property is computationally decidable (possibly with further tweaks, e.g. modulo some oracle, or with complexity constraints) or whether some object is computable (see above), express decision/construction procedures etc.; it's just incredibly clunky to do so, and it may be worthwhile to introduce foundations that make it natural to talk about these things.
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?
> Intuitionist/Constructivist `true` means, "provable".
This is completely wrong. Excluded-middle `true` means "provable" and only "provable". "Impossible to disprove" is `independent`, not `true`.
Rather, in classical logic, if you can show that a statement being false would imply a contradiction, you can conclude that the statement is true.
In intuitionistic logic, you would only conclude that the statement is not false.
And, I’m not sure identifying “true” with “provable” in intuitionistic logic is entirely right either?
In intuitionistic logic, you only have a proof if you have a constructive proof.
But, like, that doesn’t mean that if you don’t have a constructive proof, that the statement is therefore not true?
If a statement is independent of your axioms when using classical logic, it is also independent of your axioms when using intuitionistic logic, as intuitionistic logic has a subset of the allowed inference rules.
If a statement is independent, then there is no proof of it, and there is no proof of its negation. If a proposition being true was the same thing as there being a proof of it, then a proposition that is independent would be not true, and its negation would also be not true. So, it would be both not true and not false, and these together yield a contradiction.
Intuitionistic logic only lets you conclude that a proposition is true if you have a constructive/intuitionistic proof of it. It doesn’t say that a proposition for which there is no proof, is therefore not true.
As a core example of this, in intuitionistic logic, one doesn’t have the LEM, but, one certainly doesn’t have that the LEM is false. In fact, one has that the LEM isn’t false.
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.
For example, malloc returns either null or a pointer. That is an "or" type, but C can't represent that. I use an if statement to decide which (or-elimination), and then call exit() in case of a null. exit() returns an empty type, but C can't represent that properly (maybe a Noreturn function attribute). I wrap all of this in my own malloc_or_error function, and I conclude that it will only return a valid pointer.
Instead of automating a correctness proof in a different language, I run it in my own head. I can make mistakes, but it still helps me write better code.
I don't know who "we" are, but most proofs of algorithm correctness use classical logic.
Also, there's nothing "obvious" about what you said unless you want proof objects, and why you'd want that is far from obvious in itself.
I've been using formal methods for years now and have yet to see where constructive logic makes things easier (I'm not saying it necessarily makes things harder, either).
I challenge you on "most proofs of algorithm correctness use classical logic". That means double negation elimination, or excluded middle. I bet most proofs don't use those. Give examples.
You might also add designing an algorithm to begin with, or porting it from a less restrictive to a more restrictive model of computation, as kinds of proofs in CS that are closely aligned to what we'd call constructive.
Because if they benefited from it (in surfacing computational content, which is the whole point of constructive proof) they'd be comprised within the algorithm, not the proof.
The point of a constructive proof is that the proof itself is in some way computational [1], not that the algorithm is. When I wrote formal proofs, I used either TLA+ or Isabelle/HOL, neither of which are constructive. It's easy to describe the notion of "constructive computation" in a non-constructive logic without any additional effort (that's because non-constructive logics are a superset of constructive logics; i.e. they strictly admit more theorems).
[1]: Disregarding computational complexity
True, but this requires using different formal systems for the algorithm and the proof. Isabelle/HOL being non-constructive means you can't fully express proof-carrying code in that single system, without tacking on something else for the "purely computational" added content.
You are right that when using non constructive logics, it's not guaranteed that the proof is executable as a program, but that's not a downside. Having the proof be a program in some sense is interesting, but it's not particularly useful.
This is exactly how TLA+ works: https://pron.github.io/posts/tlaplus_part3
Interestingly, we handle static analysis the same way by using language subsets. The larger chunk is unprovable. So, we just work with what's easy to analyze. Then, wrap it in types or contracts to use it properly.
And plenty of testing for when the specs are wrong.
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.
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.
No, you don't.
(You need to replace the parallel postulate with a different one)
Specifically for people who are interested it seems you have to replace the parallel postulate with a postulate that says every point is a saddle point (which is like the centre point of a pringle if you know what that looks like).
A: this statement (A) is false
In classical logic, statements are either true or false. So suppose A is true. If A is true, then it therefore must be false. But suppose A is false. Well if it is false then when it says it is false it is correct and therefore must be true.
Now there are various ways in classical logic [1] to resolve this paradox but in general there is a category of things for which the law of the excluded middle seems unsatisfactory. So intuitionist logic would allow you to say that A is neither true nor false, and working in that framework would allow you to derive different results from what you would get in classical logic.
It’s important to realise that when you use a different axiomatic framework the results you derive may only be valid in the alternative axiomatic system though, and not in general. Lean (to bring this back to the topic of TFA) allows you to check what axioms you are using for a given proof by doing `#print axioms`. https://lean-lang.org/doc/reference/latest/ValidatingProofs/...
[1] eg you can say that all statements include an implicit assertion of their own truth. So if I say “2 + 2 = 4” I am really saying “it is true that 2+2=4”. So the statement A resolves to “This statement is true and this statement is false”, which is therefore just false in classical logic and not any kind of paradox.
This kind of wElL AcTUaLly argument is not allowed in constructive logic.
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.
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.
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.
Mathlib defines `by_contradiction` as a theorem proving `(¬p → False) → p` for any proposition p. ( https://leanprover-community.github.io/mathlib4_docs/Mathlib... ) This does require classical logic.
For what's happening with `¬p -> F`, recall that this is by definition the statement `¬¬p`; classical logic will let you conclude `p` from `¬¬p`, or it will let you apply the law of the excluded middle to conclude that either `p` or `¬p` must be the case, and then show that since it isn't `¬p`, it must be `p`. (Again, not really different approaches, but perhaps different in someone's mental model.)
On the other hand, if you have `p -> F`, that is by definition the statement `¬p`, and if you've established `¬p`, you've already finished proving that p is false.
Something that I find particularly absurd about the hypothetical distinction between intuitionistic and classical logic is that intuitionistic logic is sufficient to prove `¬p` from `¬¬¬p`. (This is quite similar to how 'proof by contradiction' is constructive if you're proving a negative but not if you're proving a positive; it might be the same result.) So for any proposition that can be restated in a "negative" way, the law of the excluded middle remains true in intuitionistic logic. The difference lies only in "fundamentally positive" propositions. (You can do that proof yourself at https://incredible.pm/ ; it's in section 4, `((A→⊥)→⊥)→⊥` -> `A→⊥`.)
There's a fun article on this very blog telling a similar story: https://lawrencecpaulson.github.io/2021/11/24/Intuitionism.h...
> Martin-Löf designed his type theory with the aim that AC should be provable and in his landmark Constructive mathematics and computer programming presented a detailed derivation of it as his only example. Briefly, if (∀x : A)(∃y :B) C(x,y) then (∃f : A → B)(∀x : A) C(x, f(x)).
> Spoiling the party was Diaconescu’s proof in 1975 that in a certain category-theoretic setting, the axiom of choice implied LEM and therefore classical logic. His proof is reproducible in the setting of intuitionistic set theory and seems to have driven today’s intuitionists to oppose AC.
> It’s striking that AC was seen not merely as acceptable but clear by the likes of Bishop, Bridges and Dummett. Now it is being rejected and the various arguments against it have the look of post-hoc rationalisations. Of course, the alternative would be to reject intuitionism altogether. This is certainly what mathematicians have done: in my experience, the overwhelming majority of constructive mathematicians are not mathematicians at all. They are computer scientists.
I tend to agree with the opposition on this one. Concluding that p is false because its truth leads to a contradiction is fundamentally identical to concluding that p is true because its falsity leads to a contradiction... and in particular, it is reasonable to describe 'concluding that p is false because its truth leads to a contradiction' as a 'proof by contradiction'.
The reason that the first type is "constructive" while the second one isn't is due to a strange definition of falsity on the part of the constructivists.
You can actually make that a rigorous statement in linear logic, which reintroduces the duality that's lost in intuitionistic logic while still making it possible to assess whether some claim is constructive. But linear logic is significantly more complex than either classical or intuitionistic logic.
But now I see from what you mentioned that this means that if you don't do the negation elimination, then you can still show `¬¬p` in an intuitionistic logic system.
Is proof by contradiction of a false statement just a counterexample? Because a counterexample shows that the statement is incoherent, so the negation must be true. And you have to construct a counterexample.
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.
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.
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
Denial
Anger
Bargaining
Depression
Acceptance
A talk about constructive mathematics by Andrej Bauer at the Institute for Advanced Study.
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.
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.
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!"
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.
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”.
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.
AI needs community libraries if there is to be interoperability and baseline quality between systems. At least at this level of quality and development.
I'm here saying this "PL ossification theory" is probably wrong, that it's not going to be the case at all. Yes, AI depends on training data, but that doesn't imply that AI can only use those programming languages or only reason in languages that existed at the time of their training. In fact the AI is able to reason able new languages the same way humans can -- by drawing inferences to the next closest language that it knows, pattern matching to things that are different from other languages, and also figuring out the semantics and reasoning through execution itself where it doesn't have training examples.
> AI needs community libraries if there is to be interoperability and baseline quality between systems.
Not everyone is looking to do the kind of work you're doing, and that's my point. Up until now, programming languages have been written by and for people who want to do businey/mathy/sciencey things with computers. But there's a huge world out there of other stuff to do with programming languages that have never been considered because the proposition of making languages for those domains is daunting and outside of the wheelhouse of normal people.
Now, DSLs are sprouting up where they have no business existing because of AI, just proliferating all over the place. Some of them are going to find communities (of people, AI, or both) and they will flourish completely apart from the systems we are building now in the tech world. It's not going to be the case that AI writes in Python for the rest of time because it writes in and was trained on Python today.
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.
'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.
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?
> 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.
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.
Occasionally, inspecting that proof term is useful to see what happened in a proof.
Then again, I also like dependent types.
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.
Then, ML grew into a general-purpose programming language (both OCaml and Standard ML are dialects).
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.
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.
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.
> 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”
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?)
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).
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.
Is that enough reason?
I am tired of my time in tech being just using MS products that all depend on each other.
also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.
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.
Not always.
If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.
I trust you have some examples of this?
What you've done here is an overgeneralization. "People who like math" and "people who like computers" are massive demographics with considerable overlap.
Maybe. But more clearly one of the most popular online.
The topic being discussed here has been addressed specifically in his mastodon posts - the pre-LLM math process was understood to be "state a proof, validate a proof" - but the real aim was the not explicit "digest the proof so we can extend to other results" - with LLM/lean making the first two a lot easier and possible to do without accomplishing the digestion into the mathematical community; so we need to add "digesting proofs (from where ever)" into the job description. Thread starts here: https://mathstodon.xyz/@tao/116477351524980995
I of course fully support reinstating logicism, but the same dogmatics love putting up a fight over that as well.
Putting that aside, to make things more clear: computer science is mathematics. Computer scientists are mathematicians. That was a categorization decided long before you and I ever lived. In the sense that you mean, you're only referring to a very small fraction of what "mathematics" refers to In the true sense of the word. It is just as irreconcilably disjointed as Logic is, not unified and fundamentally non-unifiable.
I too think it would be better if "mathematics" was reserved for the gated suburb of ZFC. But that's not the world we live in, courtesy of the same people who pushed ZFC as a foundation to begin with.
No. There are truths about the subject not captured in any single formal system. Which is why objects are studied form many perspectives.
> Computer scientists are mathematicians.
Some are and some aren’t.
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.
For the pragmatists Logic as a field commits the immortal sin: it blasphemes the intuition that mathematicians spend years honing by obliterating it. Not just for a singular domain, but for all domains. Of course, that doesn't really explain the whole picture. Formalism built a holy walled city. Logicians, by nature of their work, leave the safety of the walled city to survey, exploit and die in the tangled jungle outside. Some don't even speak the holy language of the glorious walled city, they talk in absolutely gibberish modalities and hyperstructures. There is a political tension held against logic and logicians as a result.