sinhp's Stars
TwoFX/sudoku
A sudoku game where you have to prove that your deductions are valid
digama0/lean4lean
Lean 4 kernel / 'external checker' written in Lean 4
Paper-Proof/paperproof
Lean theorem proving interface which feels like pen-and-paper proofs.
leanprover-community/lean4game
Server to host lean games.
leanprover-community/lean4-metaprogramming-book
nielsenramon/chalk
Chalk is a high quality, completely customizable, performant and 100% free Jekyll blog theme.
andrewbanchich/forty-jekyll-theme
A Jekyll version of the "Forty" theme by HTML5 UP.
karpathy/llama2.c
Inference Llama 2 in one file of pure C
CMU-HoTT/serre-finiteness
kbuzzard/IISc-experiments
Some material for Lean 4 lectures at IISc
siddhartha-gadgil/Superficial
Curves and other structures on surfaces (topology)
lucidrains/PaLM-rlhf-pytorch
Implementation of RLHF (Reinforcement Learning with Human Feedback) on top of the PaLM architecture. Basically ChatGPT but with PaLM
python-poetry/poetry
Python packaging and dependency management made easy
paolocrosetto/ERC_inflow_outflow
Repo to hold the ERC data and the plot of the attractiveness of EU countries in term of ERC grantees
mattrobball/lean-autograding
Setup for autograding of Lean homework using GitHub Classroom
blanchette/logical_verification_2021
leanprover/lean.js
Lean ported to Javascript with Emscripten
leanprover/lean-client-js
PatrickMassot/verbose-lean4
Natural language tactics to teach mathematics using Lean 4
PatrickMassot/lean-gym
PatrickMassot/leanblueprint
plasTeX plugin to build formalization blueprints.
osj1961/giam
A gentle introduction to the art of mathematics -- open source text for an "intro to proofs" course
adyavanapalli/natural-number-game-solutions
Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
alexeygumirov/pandoc-beamer-how-to
PatrickMassot/lean-verbose
Very controlled natural language tactics for Lean
thehottgame/TheHoTTGame
Attracting mathematicians (others welcome too) with no experience in proof verification interested in HoTT and able to use Agda for HoTT
andrejbauer/alg
Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.
tikzit/tikzit
pgf/TikZ diagram editor