Lean and Julia

[raman_kumar]

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?

Lean (proof assistant)

[technocrat]

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

[Eben60]

@raman_kumar

I see no discussion in Julia community about Lean.

SciLean language: Interactive and mathematicaly sound code transformations

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…

[foobar_lv2]

@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”.

[slwu89]

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://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.
• GitHub - ztangent/Julog.jl: A Julia package for Prolog-style logic programming.

[jar1]

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

[philzook58]

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 (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 . 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!