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