Lean
From MaRDI portal
Software:27041
swMATH15148MaRDI QIDQ27041FDOQ27041
Author name not available (Why is that?)
Source code repository: https://github.com/leanprover/lean
Cited In (74)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support
- Herbrand constructivization for automated intuitionistic theorem proving
- Verification of dynamic bisimulation theorems in Coq
- 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
- A web-based toolkit for mathematical word processing applications with semantics
- Interpreting mathematical texts in Naproche-SAD
- Maintaining a library of formal mathematics
- On a machine-checked proof for fraction arithmetic over a GCD domain
- Title not available (Why is that?)
- A Coq formalization of Lebesgue integration of nonnegative functions
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- Title not available (Why is that?)
- Friends with Benefits
- Aligning concepts across proof assistant libraries
- MODULARITY IN MATHEMATICS
- Formalizing geometric algebra in Lean
- A language with type-dependent equality
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types
- Title not available (Why is that?)
- Formalizing Galois Theory
- Bar Induction is Compatible with Constructive Type Theory
- A certified program for the Karatsuba method to multiply polynomials
- Declarative Proof Translation (Short Paper)
- Deep Generation of Coq Lemma Names Using Elaborated Terms
- Title not available (Why is that?)
- Semantic representation of general topology in the Wolfram language
- An extensible equality checking algorithm for dependent type theories
- The homological arrow polynomial for virtual links
- Title not available (Why is that?)
- Program logic for higher-order probabilistic programs in Isabelle/HOL
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Verified interactive computation of definite integrals
- Relational parametricity and quotient preservation for modular (co)datatypes
- RustHorn: CHC-Based Verification for Rust Programs
- The Lean 4 theorem prover and programming language
- A henkin-style completeness proof for the modal logic S5
- Biform theories: project description
- The Isabelle/Naproche natural language proof assistant
- A bi-directional extensible interface between Lean and Mathematica
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
- From LCF to Isabelle/HOL
- Voting theory in the Lean theorem prover
- Experiences from exporting major proof assistant libraries
- A proof strategy language and proof script generation for Isabelle/HOL
- Homotopy type theory in Lean
- Meaning explanations at higher dimension
- Implementing type theory in higher order constraint logic programming
- Title not available (Why is that?)
- Congruence Closure in Intensional Type Theory
- Semantics of Mizar as an Isabelle object logic
- Verification of the ROS NavFn planner using executable specification languages
- Univalent polymorphism
- Higher Groups in Homotopy Type Theory
- Hammer for Coq: automation for dependent type theory
- An introduction to univalent foundations for mathematicians
- Bellerophon: tactical theorem proving for hybrid systems
- Title not available (Why is that?)
- Verified Decision Procedures for Modal Logics.
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean}
- Eliminating dependent pattern matching without K
- Characteristics of de Bruijn’s early proof checker Automath
- Schemes in Lean
- Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types
- Title not available (Why is that?)
- Elaborating dependent (co)pattern matching: No pattern left behind
- Equality Checking for General Type Theories in Andromeda 2
- A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Formalization of Forcing in Isabelle/ZF
- Validating Mathematical Structures
- Title not available (Why is that?)
- Lean formalization of Vitali convergence theorem
This page was built for software: Lean
