# Lean and Julia

**URL:** <https://discourse.julialang.org/t/lean-and-julia/131424>\
**Category:** Teaching & Outreach\
**Tags:** offtopic, community\
**Created:** [August 6, 2025, 11:19pm UTC](https://discourse.julialang.org/t/lean-and-julia/131424 "2025-08-06T23:19:31Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![raman\_kumar](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/raman_kumar/32/26782_2.png) [@raman\_kumar](https://discourse.julialang.org/u/raman_kumar)\
**Post date:** [August 6, 2025, 11:19pm UTC](https://discourse.julialang.org/t/lean-and-julia/131424/1 "2025-08-06T23:19:31Z")

</div>

There are a lot of gossips/news about [Lean language](https://lean-lang.org/) for use in mathematics. I see no discussion in Julia community about Lean.

- Can Julia be used for the works that Lean do?

- Are there some areas/points where both Julia and Lean can be used together? 👫

> **[Lean (proof assistant)](https://en.wikipedia.org/wiki/Lean_(proof_assistant))**
>
> Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. It is an open-source project hosted on GitHub. Development is currently supported by the non-profit Lean Focused Research Organization (FRO). 
> Lean was developed primarily by Leonardo de Moura while employed by Microsoft Research and now Amazon Web Services, and has had significant contributions from other coauthors and collaborators during its history.
> It was laun...

---

<div class="post-metadata">

**Author:** ![technocrat](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/technocrat/32/220947_2.png) [@technocrat](https://discourse.julialang.org/u/technocrat)\
**Post date:** [August 7, 2025, 12:49am UTC](https://discourse.julialang.org/t/lean-and-julia/131424/2 "2025-08-07T00:49:40Z")

</div>

Something along these lines?

```julia-auto
abstract type Nat end
struct Zero <: Nat end
struct Succ <: Nat
    pred::Nat
end

zero() = Zero()
succ(n::Nat) = Succ(n)

function add(n::Nat, m::Zero)
    n
end

function add(n::Nat, m::Succ)
    succ(add(n, m.pred))
end

# Helper to convert to Int for testing
function to_int(n::Zero)
    0
end

function to_int(n::Succ)
    1 + to_int(n.pred)
end

# Helper to create Nat from Int
function from_int(n::Int)
    n == 0 ? zero() : succ(from_int(n-1))
end

# Test
n1 = from_int(2) # succ(succ(zero()))
n2 = from_int(3) # succ(succ(succ(zero())))
result = add(n1, n2)
println(to_int(result)) # prints 5

```

---

<div class="post-metadata">

**Author:** ![Eben60](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/eben60/32/13475_2.png) [@Eben60](https://discourse.julialang.org/u/Eben60)\
**Post date:** [August 7, 2025, 9:51am UTC](https://discourse.julialang.org/t/lean-and-julia/131424/3 "2025-08-07T09:51:44Z")

</div>

> [@raman\_kumar](#):
>
> I see no discussion in Julia community about Lean.

> [@SciLean language: Interactive and mathematicaly sound code transformations](https://discourse.julialang.org/t/scilean-language-interactive-and-mathematicaly-sound-code-transformations/81101):
>
> For quite some time I have been playing around with the idea what the next generation scientific computing language might look like and I would like to share my prototype. Mainly because Julia users are the kind of people I’m targeting and you might find it interesting. In no way I’m here to compete with Julia, this is purely experimental thing but I would like to get some feedback, opinions and some ideas on what should I focus. The library is written in Lean 4 which is a language that allows…

---

<div class="post-metadata">

**Author:** ![foobar\_lv2](https://avatars.discourse-cdn.com/v4/letter/f/ee59a6/32.png) [@foobar\_lv2](https://discourse.julialang.org/u/foobar_lv2)\
**Post date:** [August 7, 2025, 1:47pm UTC](https://discourse.julialang.org/t/lean-and-julia/131424/4 "2025-08-07T13:47:15Z")

</div>

> [@raman\_kumar](#):
>
> Are there some areas/points where both Julia and Lean can be used together? 👫

I don’t think that lean is so good a fit for julia, unfortunately. It misses all the important abstractions for interop.

Think about how computers / software work: You have a variety of “frontend” languages, like julia, C, python, etc. Then you have an ultimate backend, like the x64 ISA used by your CPU. Somewhere in the middle you have your ABI and OS.

E.g. Metamath is a backend.

But Lean, Coq, Isabelle, mizar, etc afaiu don’t use a real backend, they bring their own, which is inexorably tied to their high-level abstractions and language. It’s as terrible as the “C virtual machine”.

This is of course bad for interop, i.e. proving one lemma in lean, another in coq, and tying it together in mizar, hitting compile, and generating a proof that can be verified independently of any of these frameworks.

Until formal mathematics gets its act together, I see no really fruitful intersections.

To give a hypothetical example: I need some stupid estimates about some specific polynomial proven, because it appears in the specific ODE I want to prove facts about. In an ideal world, I’d fiddle around until I can get IntervalArithmetic.jl to generate the estimates, and then ask it to kindly output a machine verifiable proof, attach it as a 100 MB binary to my paper, and am done with this nonsense. In the real world, I fiddle around extensively, by hand, until I figure out a series of algebraic transformations that make the estimates apparent.

The same applies to UNSAT witnesses.

Unfortunately, there is no consensus on a binary proof / witness format, there is no social acceptance of this kind of workflow, and most tools don’t output reasonable witnesses, even if they strive for “proof-grade correctness”.

---

<div class="post-metadata">

**Author:** ![slwu89](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/slwu89/32/217323_2.png) [@slwu89](https://discourse.julialang.org/u/slwu89)\
**Post date:** [August 7, 2025, 2:33pm UTC](https://discourse.julialang.org/t/lean-and-julia/131424/5 "2025-08-07T14:33:01Z")

</div>

Just my 2 cents as someone who is neither a computer scientist nor mathematician but I think Julia and Lean are targeting pretty fundamentally different use cases. I’m not sure looking for integration between them would be that fruitful at this point (happy to be proven wrong).

But in some of the areas closer to Lean’s domain (SMT solvers, E-graphs, logic programming, _category theory_) there are some native Julia developments that may be interesting to you (incomplete and biased list, just what I’ve used before):

- [GitHub - JuliaSymbolics/Metatheory.jl: Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.](https://github.com/JuliaSymbolics/Metatheory.jl)
- [https://www.algebraicjulia.org/](https://www.algebraicjulia.org/) ← the whole ecosystem is built around category theory
- [GitHub - elsoroka/Satisfiability.jl: Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.](https://github.com/elsoroka/Satisfiability.jl)
- [GitHub - ztangent/Julog.jl: A Julia package for Prolog-style logic programming.](https://github.com/ztangent/Julog.jl)

---

<div class="post-metadata">

**Author:** ![jar1](https://avatars.discourse-cdn.com/v4/letter/j/c0e974/32.png) [@jar1](https://discourse.julialang.org/u/jar1)\
**Post date:** [August 7, 2025, 9:58pm UTC](https://discourse.julialang.org/t/lean-and-julia/131424/6 "2025-08-07T21:58:01Z")

</div>

I think a Julia version of @philzook58 ‘s [GitHub - philzook58/knuckledragger: A Low Barrier Proof Assistant](https://github.com/philzook58/knuckledragger/tree/main) would be great.

---

<div class="post-metadata">

**Author:** ![philzook58](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/philzook58/32/51913_2.png) [@philzook58](https://discourse.julialang.org/u/philzook58)\
**Post date:** [August 8, 2025, 3:41pm UTC](https://discourse.julialang.org/t/lean-and-julia/131424/7 "2025-08-08T15:41:45Z")

</div>

I actually did start a minimal Julia rewrapping of the python lib that I have done nothing with [GitHub - philzook58/Knuckledragger.jl: Julia Semi-Automated Proof Assistant](https://github.com/philzook58/Knuckledragger.jl)  
I’m open to the idea of Julia being a good place for this kind of system. I think the core concepts are pretty portable (rigorous chaining of z3 calls and manual quantifier instantiation). There was a port of sorts of the ideas to SBV, a haskell smt library [Data.SBV.Tools.KnuckleDragger](https://hackage.haskell.org/package/sbv-11.0/docs/Data-SBV-Tools-KnuckleDragger.html) . A speedbump to a more native Julia port is that the z3 Julia bindings aren’t as complete as the python ones last I checked.  
Advantages of such a port could include using some nice macros to make things cleaner, perf improvements from better binding to z3 and faster tactics / automated routines. Really the performance issue that worries me the most right now in the python version is that ctypes ffi is so slow.

If there are people in the Julia community that feel they would actually use such a thing, I’m all ears. Always looking for applications.

There is also the method of hooking your cart to lean by using it as an external solver [Using Lean like an External SMT Solver from Python | Hey There Buddo!](https://www.philipzucker.com/lean_smt/)

---

<div class="post-metadata">

**Author:** ![langestefan](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/langestefan/32/207923_2.png) [@langestefan](https://discourse.julialang.org/u/langestefan)\
**Post date:** [August 26, 2025, 9:18am UTC](https://discourse.julialang.org/t/lean-and-julia/131424/8 "2025-08-26T09:18:29Z")

</div>

I came across a potentially interesting intersection between Lean ([CvxLean](https://github.com/verified-optimization/CvxLean)) and Julia: [State of DCP (Disciplined Convex Programming) - #15 by langestefan](https://discourse.julialang.org/t/state-of-dcp-disciplined-convex-programming/131743/15)

Could this be worth pursuing?