Lean
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Coq
- KANT/KASH
- KeY-C
- Roosterize
- PCM library
- finmap
- ROSMonitoring
- Marathon 2
- Nitpick
- Goeland
- Cubical Agda
- Nunchaku
- jsCoq
- HolPy
- TkWinHOL
- Isabelle/HOL
- Isabelle/Isar
- CoqEAL
- Algolib
- Aligning concepts across proof assistant libraries
- Hammer for Coq: automation for dependent type theory
- Mizar
- Bellerophon: tactical theorem proving for hybrid systems
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Kenzo
- Isabelle/ZF
- Relational parametricity and quotient preservation for modular (co)datatypes
- Biform theories: project description
- Matita
- HOL Light
- QMT
- Isabelle/PIDE
- Lurch
- Univalent polymorphism
- Polar
- Verification of dynamic bisimulation theorems in Coq
- Verified interactive computation of definite integrals
- The Isabelle/Naproche natural language proof assistant
- The Lean 4 theorem prover and programming language
- AutPGrp
- Experiences from exporting major proof assistant libraries
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
- A formalization of Dedekind domains and class groups of global fields
- From the universality of mathematical truth to the interoperability of proof systems
- Flexible proof production in an industrial-strength SMT solver
- Formalizing geometric algebra in Lean
- A language with type-dependent equality
- A certified program for the Karatsuba method to multiply polynomials
- Voting theory in the Lean theorem prover
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Epigram
- Agda
- Irdis
- CalcCheck
- ForTheL
- Herbrand constructivization for automated intuitionistic theorem proving
- TLPVS
- Quantomatic
- Gmeta
- LNgen
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- On a machine-checked proof for fraction arithmetic over a GCD domain
- Maintaining a library of formal mathematics
- Interpreting mathematical texts in Naproche-SAD
- From LCF to Isabelle/HOL
- Semantics of Mizar as an Isabelle object logic
- Poly/ML
- Coquelicot
- Semantic representation of general topology in the Wolfram language
- A web-based toolkit for mathematical word processing applications with semantics
- A proof strategy language and proof script generation for Isabelle/HOL
- Manip
- Autoref
- Eisbach
- Vellvm
- Aglet
- Metamath
- dedukti
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- McBits
- A Coq formalization of Lebesgue integration of nonnegative functions
- A bi-directional extensible interface between Lean and Mathematica
- Verification of the ROS NavFn planner using executable specification languages
- A henkin-style completeness proof for the modal logic S5
- MathScheme
- UniMath
- HoTT
- Congruence closure in intensional type theory
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- MedOlDatschgerl
- AUTO2
- Globular
- Friends with benefits. Implementing corecursion in foundational proof assistants
- miz3
- CoqMTU
- CkAnalytic
- The Cayley-Dickson construction in homotopy type theory
- XBarnacle
- Pilsner
This page was built for software: Lean
