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
Tools for computer assisted proofs in analysis Specific Domains question , jump , intervals	13	1383	April 29, 2024
About operators & some other questions & possible suggestions New to Julia	8	1409	June 7, 2019
Porting a CAS to Julia General Usage	21	4038	April 24, 2018
At present, in what aspects is Julia still relatively weak compared to other mainstream programming languages? New to Julia question	63	10010	February 4, 2024
Symbolic computation in Julia with lisp/reduce; and calling Julia from LaTeX Internals & Design package , proposal	32	7959	October 29, 2020

Lean and Julia

Related topics