There are a lot of gossips/news about Lean language 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? :woman_and_man_holding_hands: [im…

Something along these lines? 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 functio…

[image] raman_kumar: I see no discussion in Julia community about Lean. [image] SciLean language: Interactive and mathematicaly sound code transformations Offtopic For quite some time I have been playing around with the idea what the next generation scie…

[image] raman_kumar: Are there some areas/points where both Julia and Lean can be used together? :woman_and_man_holding_hands: 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: Y…

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 a…

I think a Julia version of @philzook58 ‘s GitHub - philzook58/knuckledragger: A Low Barrier Proof Assistant would be great.

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 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 (rigoro…

I came across a potentially interesting intersection between Lean ( CvxLean ) and Julia: State of DCP (Disciplined Convex Programming) - #15 by langestefan Could this be worth pursuing?

Lean and Julia

Community Teaching & Outreach

Eben60 August 7, 2025, 9:51am 3

Topic		Replies	Views
Formalizing Julia in Lean (and finding 400+ bugs in Base) General Usage	22	2648	October 30, 2026
SciLean language: Interactive and mathematicaly sound code transformations Offtopic announcement	7	1630	September 24, 2024
Tools for computer assisted proofs in analysis Specific Domains question , jump , intervals	13	1559	April 29, 2024
About operators & some other questions & possible suggestions New to Julia	8	1459	June 7, 2019
Porting a CAS to Julia General Usage	21	4135	April 24, 2018

Lean and Julia

Related topics