andrejbauer / formalized-mathematics-in-lean
A graduate course on formalized mathematics at the Faculty of Mathematics and Physics, University of Ljubljana, Fall semester 2024/25
☆20Updated this week
Related projects ⓘ
Alternatives and complementary repositories for formalized-mathematics-in-lean
- A type theory with native support for Polynomial Functors.☆38Updated last year
- ☆22Updated 2 weeks ago
- A bottom-up approach to a verified implementation of MLTT☆15Updated this week
- A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming lan…☆17Updated 9 months ago
- An implementation of a simple Neural network in Idris using category theory.☆22Updated last month
- Mechanizations of Type Theories☆27Updated this week
- Reference sheet for people who know Lean 3 and want to write tactic-based proofs in Lean 4☆24Updated 3 weeks ago
- Toy implementation of Martin-Löf Type Theory☆28Updated 2 years ago
- ☆35Updated 3 years ago
- ☆22Updated this week
- Organize mathematical thoughts☆19Updated last year
- Formalization of the polymorphic lambda calculus and its parametricity theorem☆33Updated 5 years ago
- A Seamless, Interactive Tactic Learner and Prover for Coq☆57Updated 2 weeks ago
- An attempt towards univalent classical mathematics in Cubical Agda.☆29Updated last year
- 🪆 A Staged Type Theory☆34Updated last year
- Type Checking in Lean 4☆24Updated 2 months ago
- 🦠 An experimental elaborator for dependent type theory using effects and handlers☆32Updated last year
- Coq Enhancement Proposals☆45Updated this week
- Graphical rewriting for diagrammatic reasoning in monoidal categories in Lean4☆23Updated 4 months ago
- A Lean4 Formalization of Polynomial Functors☆15Updated 3 months ago
- ♾️ A library for universe levels and universe polymorphism☆33Updated last month
- ☆28Updated last year
- A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) an…☆23Updated 2 years ago
- Ring, field, lra, nra, and psatz tactics for Mathematical Components☆32Updated 2 months ago
- This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the pack…☆28Updated 5 years ago
- Set up a specific version of Agda for your GitHub Actions workflow.☆26Updated 3 weeks ago
- formalization of an equivariant cartesian cubical set model of type theory☆19Updated 3 months ago
- Class instances for Coq inductive types with little boilerplate☆24Updated 6 months ago
- A tutorial on how Agda infers things☆35Updated 3 years ago