Lean 4: Future General-Purpose Language or Niche Tool?

Stream: Lean for teaching

[Soltani Mehrez]

Hi everyone,

After several months learning Lean 4, I've been wondering about its future as a general-purpose programming language (beyond formal verification).

Questions I'm pondering:

1. Can Lean become mainstream for software development?

• Does Lean 4 have the potential to replace languages like Python, Rust, or Haskell in certain domains?
• Or will it remain primarily an academic/formal verification tool?

2. Lean's theoretical advantages in production:

• Ultra-powerful type system (dependent types)
• Formal guarantees (zero logic bugs)
• Performance (compiles to C)
• Advanced metaprogramming

But is this enough against mature ecosystems (npm, PyPI, crates.io)?

3. Real-world use cases outside academia:

Where do you see Lean 4 being adopted in industry in 5-10 years?

• Finance (critical algorithms)?
• Blockchain/Crypto (verified smart contracts)?
• AI (reasoning systems)?
• Safety-critical embedded systems?
• Other?

Barriers to adoption:

• Very steep learning curve
• Lack of libraries for standard development (web, databases, etc.)
• Few trained developers
• Limited documentation compared to Python/JS

5. Comparison with other formal languages:

How does Lean position itself against:

• Coq (academic, mature but complex)
• Agda (research-oriented)
• Idris (dependently-typed programming)
• Rust (safety without full formal proofs)

My personal intuition:

I think Lean 4 could evolve into a hybrid language:

• Core business logic = Lean (formally verified)
• Glue code / I/O = Other language

Similar to how we use C for critical parts and Python for the rest.

Open question:

In 10 years, will we see "Lean Developer" job postings for non-academic applications?

Or will Lean's future remain primarily in formal verification of code written in other languages?

---

I'm curious to hear perspectives from those who:

• Use Lean in industry
• Have experience with other proof assistants
• Work in critical domains (aerospace, finance, security)

Thanks in advance for your insights!

Personal context: I'm a mathematics teacher (18 years) with a master's in applied CS, currently creating a dataset of pedagogical proofs in Lean 4 for AI training. I'm wondering about the long-term evolution of this investment.

[Kim Morrison]

@Soltani Mehrez, I think this might be an appropriate moment to link to something I helped write long ago: https://mathoverflow.net/help/how-to-ask.

If you're going to ask a question requesting that the respondent does a lot of work for you, then it is essential (both for the sake of basic civility, and in order to get good answers) that your question demonstrates that you have already done a commensurate amount of work preparing a good question!

This question (particularly given that it is evoking :bot: emoji's from readers!) does not reach that bar.

[Soltani Mehrez]

@Kim Morrison - Thank you for the constructive feedback and the link to the guide.

You're right, my initial question was too broad. Let me provide concrete context by showing my work.

My project:
I'm creating pedagogical formal proofs in Lean 4,

Sample proofs:

• mul_conj_calc: z * conj(z) = z.re² + z.im² (12 explicit steps)
• add_conj_calc: z + conj(z) = 2 * z.re
• sub_conj_calc: z - conj(z) = 2i * z.im
• linear_combination: Combined application

My approach:
Unlike Mathlib (optimized for automation), my proofs are designed for teaching: every step is visible, justified, and annotated.

Reformulated question:
I'm at a decision point: scale this work to several hundred proofs (~6 months investment) or pivot.

Hence my question about Lean's future: I'm trying to understand whether the market will develop more toward:

• Formal verification (current dominant use case)
• Education and AI training (my current focus)
• Both

What I've already researched:

• Lean FRO vision
• Industrial adoption (mainly crypto/blockchain)
• Comparisons with Coq/Agda

Specific question:
For those with long-term experience in the ecosystem: do you see a viable market for pedagogically-oriented, formally verified content in Lean 4, beyond academic research?

Thanks for maintaining quality standards here, and apologies for the initial overly-general question. :folded_hands:

[Soltani Mehrez]

@Kim Morrison
Let me show my work
Sample proof (showing pedagogical calc-chain style):

import Mathlib.Data.Complex.Basic
open ComplexConjugate
open Complex


theorem mul_conj_1 (z : ℂ) :
  z * conj z = (z.re^2 + z.im^2 : ℝ) := by

  apply Complex.ext
  ·
    calc
      (z * conj z).re
          = z.re * (conj z).re - z.im * (conj z).im := rfl
      _   = z.re * z.re - z.im * (-z.im) := rfl
      _   = z.re * z.re - (-(z.im * z.im)) := by rw [mul_neg z.im z.im]
      _   = z.re * z.re + z.im * z.im := sub_neg_eq_add (z.re * z.re) (z.im * z.im) ▸ rfl
      _   = z.re^2 + z.im^2 := (pow_two z.re).symm ▸ (pow_two z.im).symm ▸ rfl
      _   = ((z.re^2 + z.im^2 : ℝ) : ℂ).re := rfl
  ·
    calc
      (z * conj z).im
          = z.re * (conj z).im + z.im * (conj z).re := rfl
      _   = z.re * (-z.im) + z.im * z.re := rfl
      _   = -(z.re * z.im) + z.im * z.re := by rw [mul_neg  z.re z.im ]
      _   = -(z.re * z.im) + z.re * z.im := mul_comm z.im z.re ▸ rfl
      _   = 0 := neg_add_cancel (z.re * z.im)
      _   = ((z.re^2 + z.im^2 : ℝ) : ℂ).im := rfl



theorem add_conj_1 (z : ℂ) : z + conj z = (2 * z.re : ℝ) :=
  Complex.ext
    (show (z + conj z).re = ((2 * z.re : ℝ) : ℂ).re from
      calc (z + conj z).re
          = z.re + (conj z).re := rfl
        _ = z.re + z.re := rfl
        _ = 2 * z.re := (two_mul z.re).symm
        _ = ((2 * z.re : ℝ) : ℂ).re := rfl)

    (show (z + conj z).im = ((2 * z.re : ℝ) : ℂ).im from
      calc (z + conj z).im
          = z.im + (conj z).im := rfl
        _ = z.im + (-z.im) := rfl
        _ = z.im - z.im := (sub_eq_add_neg z.im z.im).symm
        _ = 0 := sub_self z.im
        _ = ((2 * z.re : ℝ) : ℂ).im := rfl)



theorem sub_conj_1 (z : ℂ) : z - conj z = (2 * z.im : ℝ) * I :=
  Complex.ext
    (show (z - conj z).re = ((2 * z.im : ℝ) * I).re from
      calc (z - conj z).re
          = z.re - (conj z).re := rfl
        _ = z.re - z.re := rfl
        _ = 0 := sub_self z.re
        _ = (2 * z.im) * 0 - 0 * 1 := by rw [mul_zero, zero_mul, sub_zero]
        _ = (2 * z.im) * I.re - 0 * I.im := by rw [Complex.I_re, Complex.I_im]
        _ = ((2 * z.im : ℝ) * I).re := rfl)
    (show (z - conj z).im = ((2 * z.im : ℝ) * I).im from
      calc (z - conj z).im
          = z.im - (conj z).im := rfl
        _ = z.im - (-z.im) := rfl
        _ = z.im + z.im := sub_neg_eq_add z.im z.im
        _ = 2 * z.im := (two_mul z.im).symm
        _ = (2 * z.im) * 1 + 0 * 0 := by rw [mul_one, mul_zero, add_zero]
        _ = (2 * z.im) * I.im + 0 * I.re := by rw [Complex.I_re, Complex.I_im]
        _ = ((2 * z.im : ℝ) * I).im := rfl)

theorem application_1 (z : ℂ) :
  z * conj z +  (z + conj z) + I * (z - conj z) = ((z.re^2 + z.im^2 + 2 * z.re - 2 * z.im : ℝ) : ℂ) :=

  calc

  z * conj z +  (z + conj z) + I * (z - conj z)

  = ((z.re^2 + z.im^2 : ℝ) : ℂ) +  ((2 * z.re : ℝ) : ℂ) + I * ((2 * z.im : ℝ) * I) := by rw [mul_conj_1,add_conj_1,sub_conj_1]

    _ =  ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ): ℂ)  + (I * ((2 * z.im : ℝ) : ℂ)  * I) := by rw [mul_assoc, mul_comm I]

    _ =  ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ): ℂ)  + (((2 * z.im : ℝ) : ℂ) * I * I) := by rw [mul_assoc, mul_comm I]

    _ =  ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ): ℂ)  + (((2 * z.im : ℝ) : ℂ) * (I * I)) := by rw [mul_assoc, mul_comm I]

    _ = ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + (((2 * z.im : ℝ) : ℂ) * (-1 : ℂ )):= by rw [I_mul_I]

    _ = ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + ((2 * z.im : ℝ) : ℂ) * ((-1 : ℝ) : ℂ) := by

      rw [Complex.ofReal_neg , Complex.ofReal_one]

    _ = ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + ((2 * z.im * -1 : ℝ) : ℂ) :=

      by rw [← Complex.ofReal_mul ,mul_assoc , mul_neg ]

    _ =((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + ( (2 * (z.im * -1 ) : ℝ) : ℂ) :=

      by rw [ mul_assoc , mul_neg ]

    _ =((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + ( (2 * (-z.im ) : ℝ) : ℂ) :=

      by rw [mul_neg ,mul_one]

    _ = ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + ((-(2 * z.im ) : ℝ) : ℂ) :=

      by rw [neg_mul_eq_mul_neg ]

    _ = ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) + (-( 2 * z.im  : ℝ) : ℂ) :=

      by rw [Complex.ofReal_neg]

    _ = ((z.re^2 + z.im^2 : ℝ) : ℂ) + ((2 * z.re : ℝ) : ℂ) - (( 2 * z.im  : ℝ) : ℂ) :=

      by rw [sub_eq_add_neg]

    _ = ((z.re^2 + z.im^2 + 2 * z.re - 2 * z.im : ℝ) : ℂ) :=

      by rw [← Complex.ofReal_add, ← Complex.ofReal_sub]

[Michael Rothgang]

Thank you; that second version is measurably closer to something I could begin to answer. Let me help you by asking you a few questions:

You're saying "market" --- who is your target audience? What is their background? What are their needs and constraints? Show us if you have done some user research. (If you're doing this commercially, and it sounds like it, that's a good idea anyway.)

[Soltani Mehrez]

@Michael Rothgang - Great questions. Here's my thinking:

User research:
18 years teaching mathematics (Terminale level). I know which logical path works for learning — not just proving.

Target audiences:

1. LLM reasoning models (primary)

• Problem: Mathlib is optimized for efficiency, not pedagogy
• Need: "Atomic" step-by-step proofs on foundational concepts (complex numbers, arithmetic)
• My approach: Build the hiking trails with signposts, not just the highway

2. Math educators

• Problem: Few structured pedagogical resources in Lean
• Need: Ready-to-use material, explicit proofs, commented exercises
• Currently underserved

Market status:
I'm at the exploration phase. No customers yet — validating whether this gap (pedagogical formal proofs) is worth 6 months investment.

[Michael Rothgang]

This is not an answer to my question. And the fact that you just posted (what looks like) unchanged LLM output means I won't engage further.

Doing so is against the community rules here. Please put effort into your answers, or you may be suspended.

[Mirek Olšák]

I wonder if the reason for this is a language barrier, or this "agentic" mode that is what modern people prefer over human-to-human communication. The idea of the project and the lean file makes sense to me but there indeed seems to be a lot of LLM sauce around...

[Johan Commelin]

If there is a language barrier, I think it's fine to use translation tools (possibly even LLM), and disclose this. But you can still write your own messages, without emoji-bullet-listing everything.

[Soltani Mehrez]

@Michael Rothgang @Mirek Olšák @Johan Commelin
@Johan Commelin @Mirek Olšák @Michael Rothgang - Merci pour les retours.

Vous avez raison. J'ai utilisé l'IA pour l'anglais (je parle français, pas anglais) . Le sur-formatage venait de là.
Je serai transparent sur l'aide IA à l'avenir et plus naturel dans le style.

Merci.

[suhr]

Screenshot 2026-02-17 at 21-02-12 Translate French Text to English - Kagi Assistant.png

Note that AI performs better if you literally ask it for a translation. But anyway, I find French easier to read than bullet list AI slop even though I don't know French.

[Franz Huschenbeth]

Soltani Mehrez said:

Hi everyone,

After several months learning Lean 4, I've been wondering about its future as a general-purpose programming language (beyond formal verification).

Questions I'm pondering:

1. Can Lean become mainstream for software development?

• Does Lean 4 have the potential to replace languages like Python, Rust, or Haskell in certain domains?
• Or will it remain primarily an academic/formal verification tool?

2. Lean's theoretical advantages in production:

• Ultra-powerful type system (dependent types)
• Formal guarantees (zero logic bugs)
• Performance (compiles to C)
• Advanced metaprogramming

But is this enough against mature ecosystems (npm, PyPI, crates.io)?

3. Real-world use cases outside academia:

Where do you see Lean 4 being adopted in industry in 5-10 years?

• Finance (critical algorithms)?
• Blockchain/Crypto (verified smart contracts)?
• AI (reasoning systems)?
• Safety-critical embedded systems?
• Other?

Barriers to adoption:

• Very steep learning curve
• Lack of libraries for standard development (web, databases, etc.)
• Few trained developers
• Limited documentation compared to Python/JS

5. Comparison with other formal languages:

How does Lean position itself against:

• Coq (academic, mature but complex)
• Agda (research-oriented)
• Idris (dependently-typed programming)
• Rust (safety without full formal proofs)

My personal intuition:

I think Lean 4 could evolve into a hybrid language:

• Core business logic = Lean (formally verified)
• Glue code / I/O = Other language

Similar to how we use C for critical parts and Python for the rest.

Open question:

In 10 years, will we see "Lean Developer" job postings for non-academic applications?

Or will Lean's future remain primarily in formal verification of code written in other languages?

---

I'm curious to hear perspectives from those who:

• Use Lean in industry
• Have experience with other proof assistants
• Work in critical domains (aerospace, finance, security)

Thanks in advance for your insights!

Personal context: I'm a mathematics teacher (18 years) with a master's in applied CS, currently creating a dataset of pedagogical proofs in Lean 4 for AI training. I'm wondering about the long-term evolution of this investment.

I think it will evolve into a model, where we will have proof engineers and software engineers (ofc one person can also do both...). The verification code will be adjacent to the implementation code. Each Language has its own strengths and fills a certain niche. And when the cost of formal verification sinks, then it will also naturally integrate into the industry and move out of the academy niche, I recommend reading the CSLib Paper for a general outline of that vision.

One can also argue that the specification of Software (or a Function), might at some point be so strong, that the implementation code can be AI-hammer in any language, which has a (Lean) Verification Toolchain. Which ofc Lean has the strongest, as it is native. But in the beginning we will need Toolchains, also to maintain and then slowly migrate old code.

[Soltani Mehrez]

@Franz Huschenbeth The "Proof Engineers vs Software Engineers" idea clarifies my project thinking a lot. Thanks.

[Soltani Mehrez]

(deleted)

[Soltani Mehrez]

@suhr Thanks for this it's encouraging to read. I'll stick to writing myself from now on.