The following pages link to Lean (Q27041):
Displaying 50 items.
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Bellerophon: tactical theorem proving for hybrid systems (Q1687737) (← links)
- Homotopy type theory in Lean (Q1687770) (← links)
- Meaning explanations at higher dimension (Q1688954) (← links)
- Relational parametricity and quotient preservation for modular (co)datatypes (Q1791181) (← links)
- Biform theories: project description (Q1798949) (← links)
- Univalent polymorphism (Q1987219) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- Verified interactive computation of definite integrals (Q2055881) (← links)
- The Isabelle/Naproche natural language proof assistant (Q2055899) (← links)
- The Lean 4 theorem prover and programming language (Q2055901) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Certifying algorithms and relevant properties of reversible primitive permutations with \textsf{Lean} (Q2097420) (← links)
- A formalization of Dedekind domains and class groups of global fields (Q2102929) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Formalizing geometric algebra in Lean (Q2128117) (← links)
- A language with type-dependent equality (Q2128827) (← links)
- A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
- Voting theory in the Lean theorem prover (Q2148823) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- Herbrand constructivization for automated intuitionistic theorem proving (Q2180528) (← links)
- Designing normative theories for ethical and legal reasoning: \textsc{LogiKEy} framework, methodology, and tool support (Q2211865) (← links)
- On a machine-checked proof for fraction arithmetic over a GCD domain (Q2217198) (← links)
- Maintaining a library of formal mathematics (Q2219408) (← links)
- Interpreting mathematical texts in Naproche-SAD (Q2219411) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Semantic representation of general topology in the Wolfram language (Q2364674) (← links)
- A web-based toolkit for mathematical word processing applications with semantics (Q2364686) (← links)
- A proof strategy language and proof script generation for Isabelle/HOL (Q2405272) (← links)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge (Q2663667) (← links)
- A Coq formalization of Lebesgue integration of nonnegative functions (Q2673304) (← links)
- A bi-directional extensible interface between Lean and Mathematica (Q2673306) (← links)
- Verification of the ROS NavFn planner using executable specification languages (Q2693303) (← links)
- A henkin-style completeness proof for the modal logic S5 (Q2695534) (← links)
- Congruence Closure in Intensional Type Theory (Q2817913) (← links)
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures (Q2829996) (← links)
- Friends with Benefits (Q2988636) (← links)
- (Q3121020) (← links)
- (Q3300787) (← links)
- An introduction to univalent foundations for mathematicians (Q4684362) (← links)
- Cubical Agda: A dependently typed programming language with univalence and higher inductive types (Q5016211) (← links)
- An extensible equality checking algorithm for dependent type theories (Q5028472) (← links)
- Equality Checking for General Type Theories in Andromeda 2 (Q5041060) (← links)
- RustHorn: CHC-Based Verification for Rust Programs (Q5041108) (← links)
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis (Q5048989) (← links)
- A Lean Tactic for Normalising Ring Expressions with Exponents (Short Paper) (Q5048990) (← links)
- Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
