📐 Lean 4 vs Rocq (Coq) in 2025: Honest Assessment

Okay, I know this thread is going to get spicy and I'm prepared for the flame war. But I genuinely think we need to have a calm, evidence-based discussion about this in 2025 because the landscape has changed substantially and a lot of people are still operating on 2020-era assumptions.

Let me lay out my case for Lean 4 first, and then I expect the usual suspects to come in screaming about CompCert and Ltac.

Why I think Lean 4 has pulled ahead:

• Mathlib is enormous. As of mid-2025, mathlib had formalized over 210,000 theorems and 100,000 definitions. That's not a library, that's a civilization. Nothing in the Rocq ecosystem comes close to this breadth.
• Tactic ergonomics. The Lean 4 tactic language is just... nicer to write? simp, ring, linarith, aesop, omega — these compose beautifully. Writing a proof in Lean feels like writing code, not casting ancient incantations.
• It's also a real programming language. Lean 4 is "fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator." You can write your proof automation IN Lean and it compiles to efficient C.
• Momentum & AI tooling. DeepSeek-Prover-V2, Leanstral, every major AI theorem proving effort targets Lean 4 first. This is a feedback loop that's going to compound.
• Universe polymorphism that doesn't make you want to cry. Lean uses a non-cumulative hierarchy, Rocq uses a cumulative one. Both have trade-offs, but Lean's Sort u approach is way more predictable in practice.

Here's a comparison of proving something dead simple — commutativity of natural number addition — to show the ergonomic difference:

theorem Nat.add_comm (n m : ℕ) : n + m = m + n := by
  induction n with
  | zero => simp
  | succ n ih =>
    simp [Nat.succ_add, ih]

-- Or just: omega

That last comment is not a joke. For most arithmetic goals, omega just closes them. The degree to which Lean 4 can automate grunt work is genuinely remarkable in 2025.

I'm not saying Rocq is dead or bad. It has decades of industrial use and CompCert is still the gold standard for verified compilation. But for doing mathematics in 2025, Lean 4 is where I'd tell anyone to start.

Fight me. 🐱

Both of you are wrong because neither of you is using Agda.

I'll see myself out.

...

Okay fine, since I'm here: the elephant in the room is that both Lean 4 and Rocq are based on CIC (Calculus of Inductive Constructions), while Agda's type theory is more expressive in certain ways — particularly around universe polymorphism and without the Prop/Set/Type distinction creating weird artifacts.

In Agda you write things like:

open import Data.Nat
open import Data.Nat.Properties

-- The proof is literally: refl, from a ring solver
+-comm-demo : (n m : ℕ) → n + m ≡ m + n
+-comm-demo n m = +-comm n m

And you get proper universe-polymorphic definitions that work at any level without needing to sprinkle @[universe_polymorphism] or fiddle with Prop vs Set. The cubical Agda extension gives you actual HoTT with computational univalence.

The Lean 4 vs Rocq debate is basically two people arguing about whether Ford or Chevy is better while I'm driving a Tesla. Not perfect, but a fundamentally different vehicle.

(Library ecosystem: yes, Agda's stdlib is smaller. I know. Please don't @ me.)

Nobody has mentioned Isabelle/HOL yet and that tells me everything about the state of this community's institutional memory.

While you all fight about CIC variants, Isabelle/HOL has quietly had:

• Archive of Formal Proofs (AFP) — thousands of formalized entries covering mathematics and CS theory
• seL4 microkernel verification — an actual deployed, formally verified OS kernel, verified in Isabelle
• Sledgehammer — the original "hammer" that calls external ATPs and SMT solvers, still among the best automation out there
• Isar proof language — structured, human-readable proofs that look closer to mathematical prose than any tactic-based system

An Isar proof looks like:

theorem add_comm_nat: "(n::nat) + m = m + n"
proof (induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

The Isar language forces you to write proofs that are self-documenting. You can read an Isar proof and understand it without running it. Can you say the same for a Lean 4 tactic block that's just simp [*]; omega; aesop?

Yes, Isabelle/HOL is based on HOL (Higher-Order Logic) rather than dependent types, which means you can't express some things as cleanly. But Lean itself is "based on dependent type theory and constructs explicit proofs passed to a trusted small kernel, while Isabelle/HOL is based on higher-order logic and uses the LCF approach" — meaning Isabelle's foundational approach is arguably more conservative and well-understood.

The dark horse is here, and it's wearing a tweed jacket and publishing in the AFP. Just saying. 🐈‍⬛

First-time poster in a major thread, be gentle 🙏

I'm a PhD student who had to pick one of these for their dissertation (formal verification of a distributed consensus algorithm) and I went with Lean 4 about 8 months ago. Here's my ground-level experience:

The good (Lean 4):

• The VS Code integration with the Lean 4 infoview is genuinely magical. Seeing the proof state update in real time as you type tactics is something you can't un-experience.
• decide tactic for decidable propositions is amazing — you can just ask Lean to check small finite cases computationally.
• The omega tactic closed about 40% of my arithmetic obligations automatically. That's not a joke.
• Mathlib's Finset and Fintype infrastructure is excellent for my distributed systems work.

The rough edges (Lean 4):

• Build times. lake exe cache get is your friend but a cold build of Mathlib is still painful on anything below 16GB RAM.
• The error messages when something goes wrong in elaboration can be... cryptic. "Failed to synthesize instance" with a 3-screen stack trace is my Tuesday.
• Universe polymorphism: when you need it, you really need it, and figuring out the right universe u v incantation takes trial and error.
• Documentation for the less-traveled parts of Mathlib is sparse. You're often reading source code.

Would I switch to Rocq now? Probably not, sunk cost aside. But if I were doing something closer to program verification I'd seriously reconsider.

Also +1 to IsabelleCat on Sledgehammer. I tried an Isabelle port of one of my smaller lemmas and Sledgehammer closed it in 4 seconds where my Lean proof took an afternoon. The automation gap for first-order reasoning is real.

Jumping in with a number theory / arithmetic geometry perspective.

The reason I migrated from Rocq to Lean 4 in 2023 and haven't looked back: the FLT project. Kevin Buzzard's formalization of Fermat's Last Theorem in Lean 4 is not just a proof engineering achievement — it's reshaping how algebraic number theorists think about formalization. The community building around it is unlike anything I've seen in formal math.

Mathlib's algebraic hierarchy is genuinely impressive. Category theory, sheaves, schemes — it's all there and growing. The structure looks like:

-- Everything is built on typeclasses, composing naturally
variable {R : Type*} [CommRing R] [IsDomain R]
variable {M : Type*} [AddCommGroup M] [Module R M]

-- Lean figures out the entire typeclass hierarchy automatically
example (f : M →ₗ[R] M) : f.ker.subtype.range = ⊥ := by
  exact LinearMap.range_eq_bot.mpr (Submodule.ker_subtype _)

The typeclass synthesis — where Lean automatically figures out that an IsDomain is a NoZeroDivisors, which gives you CancelMonoidWithZero instances — happens silently and correctly. The "typeclass resolution procedure based on tabled resolution" is a genuine engineering achievement that makes Lean usable for complex algebraic reasoning at scale.

MathComp has a similar tower (eqType → choiceType → finType etc.) but it's more manual, less discoverable, and the inference is slower for deep hierarchies.

My hot take: by 2026, the Lean/Rocq debate will look like the Linux/BSD debate. Both fine, one has the momentum.

Delurking to add something practical that nobody's mentioned: what's it actually like to set up and use day-to-day?

I tried both this year as a newcomer (PhD student, CS, interested in PL theory):

Lean 4 setup: elan + lake new MyProject + add mathlib dependency + lake exe cache get. Honestly pretty smooth. The VS Code extension (lean4) just works. The infoview showing the proof state in a side panel is excellent. Took me about 20 minutes from zero to first working proof.

Rocq setup: opam (if you know what that is...), then choosing between vanilla Rocq, MathComp, or SSReflect setups, then figuring out which editor extension (VsCoq2? Proof General in Emacs?). Getting Coq installed was... a non-trivial task on M1 Mac. Proof General is powerful once you know it but the learning curve is steep. VsCoq2 is getting better but still lags behind the Lean 4 VS Code experience.

For a newcomer in 2025: Lean 4 wins the onboarding experience decisively. The barrier to entry on Rocq is real and was enough to push me toward Lean for my dissertation work. Once you're in the Rocq ecosystem it's fine, but that initial friction matters a lot.

Also: Lean's exact? and apply? tactics that search Mathlib for applicable lemmas are underrated quality-of-life features. You can describe the shape of what you need and Lean will find it. Amazing for beginners and experts alike.

This has been a remarkably good thread actually. Let me try to synthesize.

I think CoqFanatic's p6 breakdown was fair and I mostly agree with it. The "honest assessment" is not that one system is universally better, but that they occupy different niches with significant overlap:

type UseCase =
  | PureMath             -- winner: Lean 4 (Mathlib)
  | ProgramVerification  -- winner: Rocq (CompCert, VST)
  | SafetyCritical       -- winner: Isabelle (seL4) | Rocq
  | TypeTheoryResearch   -- winner: Agda (Cubical)
  | Teaching            -- winner: Lean 4 (resources) | Isabelle (Isar)
  | AITooling           -- winner: Lean 4 (by a mile)
  | IndustrialMath      -- winner: Lean 4 (trajectory)

let pick_prover (uc : UseCase) : Prover =
  match uc with
  | PureMath | Teaching | AITooling → Lean4
  | ProgramVerification → Rocq
  | SafetyCritical → Isabelle -- or Rocq
  | TypeTheoryResearch → Agda
  | IndustrialMath → Lean4 -- for now

The one thing I'll double down on: if you're choosing a first theorem prover in 2025 with no specific application in mind, pick Lean 4. The community, tooling, documentation, and AI assistance have reached a tipping point. You can always migrate later, but you'll learn the concepts fastest in Lean 4 right now.

Thanks for keeping this civil everyone. This is why I love CGPA. 🐱

[Thread continues for 190 more replies on pages 2–9, including a spectacular derail on page 3 about whether Lean 4's classical axioms constitute a moral failing, a Mizar defender who appears briefly on page 5, and CoqFanatic returning on page 7 after sleep to walk back two of their concessions.]