leanprover/lean4 on Hacker News

…lexing level. There is an example that adds HTML-like syntax and uses it later in the same file. https://github.com/leanprover/lean4/blob/0f2eaa6e776255083f9... (I'm not saying changing the language on the fly is a good idea, but it's…

comment by dunham · 2026-10-27 · in Writing about pratt parsing so I remember it

…lean are not unheard of. That's why they recommend using external checkers for "malicious" proofs. https://github.com/leanprover/lean4/issues/14576

comment by IsTom · 2026-09-12 · in Navier-Stokes Announcement

This has happened: https://github.com/leanprover/lean4/issues/14576

comment by ToValueFunfetti · 2026-09-05 · in Fermat's Last Theorem in Lean 4

…). I'm not so familiar with Lean, but it would appear its kernel is spread over this C++ directory: https://github.com/leanprover/lean4/tree/master/src/kernel . As mentioned in the article, HOL Light gets away with a lot because it only…

comment by momentoftop · 2026-08-05 · in Why is it all in the kernel?

No, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel , this part of a codebase has hardly changed since Lean 3). Almost all the space in the package (more than 2.5…

comment by unexpectedtrap · 2026-04-13 · in A perfectable programming language

…of the excluded middle using Diaconescu's theorem rather than assuming it as an independent axiom: https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...

comment by cwzwarich · 2025-08-18 · in Typechecker Zoo

…are type correct and the environment is well-formed (that is, check the correctness). [1] https://github.com/leanprover/lean4/blob/3a3c816a27c0bd45471... [2] https://github.com/digama0/oleandump [3] https://github.com/ammkrn/nanoda_lib

comment by kmill · 2025-07-31 · in The Math Is Haunted

…a lot. Nowadays I'm doing model counting and maybe synthesis, if all goes well [2] [1] https://github.com/leanprover/lean4/pulls/bollu [2] https://x.com/SoosMate/status/1827308967208317241

comment by zero_k · 2024-10-10 · in Quantum Advantage for NP Approximation

…solver did you work on? And yeah, I've been working on formally verifying bitblasting in Lean ( https://github.com/leanprover/lean4/pulls?q=+is%3Apr+author%... ), and it's genius --- the algorithms, the reductions, the heuristics, it's all…

comment by bollu · 2024-10-10 · in Quantum Advantage for NP Approximation

lean4 - programming language and theorem prover https://lean-lang.org/ https://github.com/leanprover/lean4

comment by yboris · 2024-06-12 · in Terence Tao on proof checkers and AI programs

Lean is free and open source and nothing to do with MS. Check out https://lean-lang.org/ and https://github.com/leanprover/lean4 -- no mention of MS or MSR (where de Moura was where he developed Lean 3 and started on Lean 4). I have no…

comment by kevinbuzzard · 2024-05-01 · in The Fermat's Last Theorem Project

…as the standard library. [1]: https://leanprover.github.io/functional_programming_in_lean/ [2]: https://github.com/leanprover/lean4 [3]: https://github.com/leanprover/lean4/blob/master/src/Init/Pre... [4]:…

comment by crvdgc · 2024-03-20 · in The Mechanics of Proof

…). There is an example in the source repository that adds and then uses a JSX-like syntax. ( https://github.com/leanprover/lean4/blob/master/tests/playgr... )

comment by dunham · 2023-10-27 · in Lean4 helped Terence Tao discover a small bug in his recent paper

…I found that adds a simple JSX-like syntax starting around line 93 and then uses it at line 169: https://github.com/leanprover/lean4/blob/master/tests/playgr... I believe most of the language is defined this way, although it is…

comment by dunham · 2023-05-30 · in Macro-ts: TypeScript compiler with typesafe syntactic macros (2022)

Some quick info for Lean: Homepage: https://leanprover.github.io/ Source: https://github.com/leanprover/lean4 Wikipedia: https://en.wikipedia.org/wiki/Lean_(proof_assistant)

comment by peter_d_sherman · 2023-01-20 · in Idris: A language for type-driven development

…Lean4[1] instead. They rewrote it in Lean itself and now it has much cleaner design[2][3][4]. [1] http://github.com/leanprover/lean4 [2] https://leanprover.github.io/papers/lean4.pdf [3] https://leanprover-community.github.io/lt2021/slides/…

comment by xvilka · 2022-01-24 · in Ask HN: What technology is “cutting edge” in 2022?

The author of Z3, Leo de Moura, released Lean 4 milestone 1 about 3 weeks ago: https://github.com/leanprover/lean4 Lean 4 is a functional programming language and theorem prover that compiles to C. A lot of research went into making Lean 4…

comment by tromoi21 · 2021-01-31 · in Software Verification and Analysis Using Z3

…might be a better place to start (the main development team have moved onto developing Lean 4.0 ( https://github.com/leanprover/lean4 ), and it's not clear when that will be ready).

comment by logicchains · 2020-04-06 · in Doing a math assignment with the Lean theorem prover

…performance, use a low-level language. [1] https://github.com/leanprover/lean/tree/master/src [2] https://github.com/leanprover/lean4/tree/master/src

comment by Cladode · 2020-01-24 · in Haskell Problems for a New Decade

Lean 4 WIP is public now: https://github.com/leanprover/lean4 . But PRs aren't welcome. Personally I think Coq's done waaay better at community management.

comment by logicchains · 2019-10-10 · in The Future of Mathematics? [video]

…translate nicely to other theorem provers, and especially Lean 4. Lean 4 has already gone public: https://github.com/leanprover/lean4/ Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.

comment by foooobar · 2019-09-29 · in Theorem Proving in Lean [pdf]

Where can I read more about the decision to develop Lean 4 in private, and what is the status of https://github.com/leanprover/lean4 , in your view?

comment by jbapple · 2019-09-29 · in Theorem Proving in Lean [pdf]