Pinned Repositories
advent2018
Solutions to advent of code 2018
combinatorics
epfl-comb
EPFL Combinatorics Lean notes
exponential-ramsey
floods
Haskell implementation of Flood-It
maths-notes
Lecture notes from Cambridge maths
robot-one
sunflower
topos
Topos theory in lean
unit-fractions
b-mehta's Repositories
b-mehta/maths-notes
Lecture notes from Cambridge maths
b-mehta/topos
Topos theory in lean
b-mehta/combinatorics
b-mehta/unit-fractions
b-mehta/exponential-ramsey
b-mehta/epfl-comb
EPFL Combinatorics Lean notes
b-mehta/sunflower
b-mehta/ExponentialRamsey
b-mehta/regularity-lemma
Code accompanying submission to ITP 2022
b-mehta/carleson
A formalized proof of Carleson's theorem in Lean
b-mehta/entity-linking
b-mehta/equational_theories
A project to map out the relations between different equational theories of Magmas.
b-mehta/Example-Lean-Projects
Some examples of Lean projects, for undergraduate mathematicians.
b-mehta/FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
b-mehta/generating-functions
playing with generating functions in Lean
b-mehta/human_oriented_atp
b-mehta/icfp2024
b-mehta/lean4
Lean 4 programming language and theorem prover
b-mehta/LeanProject
Template for blueprint-driven formalization projects in Lean.
b-mehta/leanprover-community.github.io
Hosts the website for mathlib and other Lean community infrastructure.
b-mehta/leanprover-contrib
b-mehta/lftcm2020
Lean for the Curious Mathematician 2020
b-mehta/linear-base
Standard library for linear types in Haskell.
b-mehta/mathematics_in_lean_source
Source code for the Mathematics in Lean tutorial.
b-mehta/mathlib
Lean mathematical components library
b-mehta/sharkovsky
b-mehta/sphere-eversion
Formalization of the existence of sphere eversions
b-mehta/std4
Standard Library for Lean 4
b-mehta/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
b-mehta/vscode-lean
An extension for VS Code which provides support for the Lean language.