The answer is Rocq and it's not even close for anything involving software verification. I've been using it since the Coq days (yes, that's what we called it before the rename), and the maturity of the ecosystem just doesn't get enough credit.

The math-comp / SSReflect tactic language is a genuine work of art. Once you understand the move=> / apply: / view mechanism, you write proofs that are incredibly dense and compositional. Compare:

Also: Rocq's foundations are genuinely more carefully designed than Lean's. Rocq has been very particular about sound type-theoretic foundations throughout its history. The Calculus of Inductive Constructions kernel has been studied extensively. Lean added things like quotient types and proof irrelevance that are convenient but introduce trust surface area.

That said — I'll admit the community mass of Mathlib4 is impressive. But "more stuff" isn't the same as "better foundations." The 35-year pedigree of Rocq is not nothing.

I'm going to be the boring centrist here: I use both and I think that's actually fine?? Different tools for different jobs, etc.

Lean 4 for pure math formalization because Mathlib4 is just... a phenomenon. The docs are good, the Zulip community answers questions within hours, and the exact? / apply? tactics make exploration so comfortable. I recently formalized something involving commutative algebra and the quotient-type support in Lean's kernel made it genuinely painless. Rocq's approach to quotienting via setoids is, and I say this with love, a special kind of suffering.

But for anything where I care about extraction and getting verified OCaml or Haskell out the other end — Rocq all the way. The MetaRocq extraction pipeline is mature and well-studied. Lean's compiled output is great for running Lean programs, but the extraction story for verified software is still younger.

The rename from Coq to Rocq is also growing on me. The naming rationale is sound — the old name had, uh, problems internationally — and the new name actually sounds like a proper software project name.

I want to push back on the "Lean's foundations are less careful" narrative because I see it repeated a lot and I think it's become a bit of a meme that doesn't reflect 2025 reality.

Lean 4's elaborator is genuinely sophisticated. The bidirectional type-checking, the metavariable unification, the typeclass resolution — these are all well-engineered. Lean is also based on the Calculus of Inductive Constructions at its core, with some deliberate extensions (definitional proof irrelevance, quotient types in the kernel). Those extensions were designed choices, not sloppiness.

The ring tactic handling that in one step is emblematic of what Mathlib4 has become. The tactic automation is ahead of anything in the Rocq ecosystem for pure mathematics, full stop.

Also: the tooling story in 2025 is dramatically in Lean 4's favor. The VS Code extension with its live infoview is miles ahead of anything Rocq offers. You can see your proof state update in real time as you type. The elaboration speed improvements in recent versions mean that even large Mathlib imports are manageable with the cache.

I'm not saying Lean 4's engineering is bad — Sebastian Ullrich and Leo de Moura are clearly world-class — I'm saying the metatheory is less developed. We have the "Coq Coq Correct!" result formalizing Rocq's engine and proving metatheoretic properties about it, in Rocq itself. We have 35 years of published meta-theory. The Lean 4 kernel is solid but it's young and less formally characterized.

On the tooling point: okay fine, VS Code + Lean 4 infoview is very nice. I'll give you that. RocqIDE is showing its age. But Proof General in Emacs is still functional and I will not hear otherwise.

The real issue I have with Lean 4 hegemony is the monoculture risk. Mathlib4 is one giant library maintained by one community with one set of design decisions. If there's a foundational issue, there's nowhere to run. Rocq's ecosystem is more fragmented, yes, but also more diverse — math-comp, UniMath, HoTT library, MetaRocq, Iris — these are real independent projects with independent design philosophies.

Also cumulativity. Rocq's universe cumulativity is a better design choice for higher category theory than Lean's explicit non-cumulative universes. Fight me.

Coming at this from a PL / type theory research angle rather than math formalization. For me the deciding factor is the metaprogramming story.

Lean 4's macro system and MetaM / TacticM / TermElabM monad stack for writing custom tactics is genuinely exceptional. The fact that Lean 4 is self-hosting — the elaborator is written in Lean 4 — means you can inspect and extend almost any part of the system. Hygenic macro expansion, notation-as-syntax-sugar, custom elab rules... the whole thing is designed for extensibility from the ground up.

Rocq's Ltac2 is a genuine improvement over Ltac1 (which had... interesting scoping rules) but it still feels like a bolted-on extension compared to Lean 4's deeply integrated elaboration monad approach. Ltac2 is good! But it's not the same level of architectural elegance.

On the other hand: Rocq 9.0's improvements to the Program command and general dependent pattern matching are substantial. The recent versions of Rocq have been moving fast.

Really appreciate the range of perspectives already. OP here. A few reactions:

@RocqCatFan — the monoculture point is fair and I think about it. But I'd argue Mathlib4's size is also a coordination achievement — everything uses consistent naming conventions, all PRs go through the same review process, you get a coherent mathematical library rather than N independent libraries with incompatible definitions of "group." The fragmentation in the Rocq ecosystem means you often can't easily combine results from math-comp and UniMath because they've made different foundational choices.

@BidirBrigade — the MetaM story is excellent and criminally underappreciated. I wrote a custom category theory tactic set last year and it was genuinely delightful. The fact that you can #check your tactic combinators as regular Lean terms is philosophically satisfying.

One thing nobody has mentioned yet: the AI tooling landscape in 2025 heavily favors Lean 4. We now have multiple serious ML models (DeepSeek Prover V2, Leanstral from Mistral, etc.) specifically targeting Lean 4 theorem proving. The training data flywheel of Mathlib4 being so large and high-quality makes this a real moat.

The AI tooling point from FormalFelinae is real and I think it's underappreciated how much it's going to matter going forward. Lean 4 is now the de facto target for formal math AI because of how large and well-structured Mathlib4 is as training data. That creates a feedback loop: better AI tools → more people using Lean 4 → more formalization → even better training data.

Rocq has the LLM4Rocq project and they're doing interesting work (the MathComp documentation effort is great for training), but it feels like Lean 4 has lapped the field here simply due to Mathlib's scale.

That said — I want to explicitly defend Rocq's Iris framework for concurrent separation logic. If you're doing program verification for concurrent systems, Iris in Rocq is just... the tool. There's no real Lean 4 equivalent for that specific use case yet. The iMod / iIntro / iApply tactics in Iris are extraordinarily well-designed for the problem domain.

You're simply not doing this in Lean 4 right now at the same maturity level. Rocq has niches where it's still clearly the right choice.

Fair on Iris, @ProofKitten. I'm not going to pretend Lean 4 wins every niche. The concurrent program verification space is genuinely Rocq territory right now.

Let me talk about something concrete that made me switch and stay: Lean 4's elaboration feedback loop. When you're working interactively, you get the proof state displayed in real time. You hover over a term, you see its type. You type a tactic, the goal updates immediately. The infoview panel in VS Code is — and I mean this sincerely — a better proof-writing experience than anything I've used in 15 years of type-theory work.

The fact that Lean 4 is also a real general-purpose programming language means I can write my tooling in Lean itself. My bespoke decision procedures, my domain-specific tactics, my notation extensions — all written in the same language, checked by the same type system, no FFI weirdness. Lean.Elab.Tactic is your friend.

One genuine weakness: build times. lake build Mathlib without cache is a commitment. The lake exe cache get pipeline works well in practice, but it's still an adventure on first setup. Rocq's math-comp builds in under 10 minutes; Mathlib takes significantly longer. This is a real usability issue that the community keeps working on.

Alright here is my honest 2025 summary as someone who has spent serious time in both:

Choose Lean 4 if:

• You want to formalize pure mathematics — Mathlib4 is unrivaled
• You care about tooling quality and IDE experience
• You want AI-assisted proof writing (DeepSeek Prover V2, Leanstral, etc.)
• You're new to proof assistants — the learning curve is more forgiving
• You want your proof assistant to also be a programming language

Choose Rocq if:

• You're doing concurrent program verification (Iris)
• You need mature program extraction to OCaml/Haskell
• You work with the math-comp / SSReflect ecosystem specifically
• You care deeply about metatheoretic properties and foundations
• You're already deeply embedded in a Rocq codebase

The honest answer is that both communities are producing incredible work and the competition is healthy. The new Babel-Formal translation tools that can convert proofs between Lean and Rocq are genuinely exciting — maybe in 5 years this debate will be moot because interoperability improves.

Also: can we appreciate that we live in a time when this is a real debate? A decade ago proof assistants were a niche academic curiosity. Now we're arguing about which excellent option to pick. We won.

...okay fine, that's a good point and I'll choose to feel good about it instead of continuing to argue. The fact that multiple serious proof assistants are genuinely competitive in 2025 is a sign of how far the field has come.

I'll be a bit less cranky and admit: the Lean 4 syntax design is genuinely nicer than anything in the Rocq world. The Unicode support, the readable theorem / def / structure / class syntax, the way where clauses let you factor out helpers... it reads more like mathematics. SSReflect is powerful but it's an acquired taste with a steep learning cliff.

What I won't concede: ssr's proof by reflection techniques, where you reduce a proposition to a boolean computation that the kernel can just evaluate, produce proofs that are incredibly compact and fast to check. Lean 4's decide tactic does something similar but the ergonomics of building large reflective decision procedures feels more awkward.

Final hill I'll die on: Rocq's universe polymorphism with cumulativity is better designed for higher-category theory than Lean 4's approach. Category theory in Lean has not been developed with ∞-categories in mind, and the non-cumulative universe design makes certain constructions genuinely painful.