Pinned Repositories
automating-mathematics
CategoryTheory
Basic category theory in Lean4
combinatornithology
A series of puzzles on combinatory logic written in LEAN, inspired by the book "To Mock a Mockingbird" by Raymond Smullyan.
formal-systems
This repository contains implementations of various formal systems such as lambda calculus, SKI combinatory calculus and propositional logic.
IISER-Pune-Type-Theory-Talks
A series of six lectures at the IISER Pune mathematics department giving a broad overview of type theory and interactive theorem provers.
lean-slides
A tool to auto-generate and render slides from Markdown comments in the Lean editor.
lean3-statement-translation-tool
A tool for automatic formalisation of natural language theorem statements to Lean3 code using OpenAI Codex.
lean4-gym
A REPL-like interface for Lean4 tactic proofs.
theorem-proving
This repository contains code for automated proofs to (or verifications of) problems, mainly from Euclidean Geometry, using the Z3 SMT solver.
0art0's Repositories
0art0/lean-slides
A tool to auto-generate and render slides from Markdown comments in the Lean editor.
0art0/lean3-statement-translation-tool
A tool for automatic formalisation of natural language theorem statements to Lean3 code using OpenAI Codex.
0art0/lean4-gym
A REPL-like interface for Lean4 tactic proofs.
0art0/combinatornithology
A series of puzzles on combinatory logic written in LEAN, inspired by the book "To Mock a Mockingbird" by Raymond Smullyan.
0art0/IISER-Pune-Type-Theory-Talks
A series of six lectures at the IISER Pune mathematics department giving a broad overview of type theory and interactive theorem provers.
0art0/theorem-proving
This repository contains code for automated proofs to (or verifications of) problems, mainly from Euclidean Geometry, using the Z3 SMT solver.
0art0/CategoryTheory
Basic category theory in Lean4
0art0/Cellular-Automata
A collection of 2-D cellular automata simulations built on pygame.
0art0/ComputationalComplexity
An attempt at formally proving runtime bounds on some standard algorithms
0art0/equational_theories
A project to map out the relations between different equational theories of Magmas.
0art0/Freudenthal-Hopf
Formalisation of the Freudenthal-Hopf theorem in Lean.
0art0/GroupComp
Lean 4 code and some slides for the NCM workshop on Groups and Computations at KREA, July 2023
0art0/lambda-cube
A blog on mathematics, foundations, computer science and more.
0art0/lean4
Lean 4 programming language and theorem prover
0art0/leandiscord-weekly
Weekly challenges for the Lean Discord Server.
0art0/LeanInk
LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
0art0/LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
0art0/math-puzzles-in-lean4
math puzzles from various sources, formalized in Lean 4
0art0/Polylean
0art0/ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
0art0/rewrite-system-interface
An implementation of rewrite systems in Lean together with a point-and-click interface for rewriting.
0art0/Saturn
Experiments with SAT solvers with proofs in Lean 4
0art0/sphere-eversion
Formalization of the existence of sphere eversions
0art0/std4
Standard Library for Lean 4
0art0/SymbolicAlgebra
Mathematical programs with proofs, in LEAN 4.
0art0/theHoTTGameGuide
0art0/tree-rewriting-game
0art0/verso
Lean documentation authoring tool
0art0/vscode-lean4
Visual Studio Code extension for the Lean 4 proof assistant
0art0/WZ
Implementation of the Gosper algorithm (an essential component of the WZ algorithm) and formalisation of the WZ theorem in LEAN.