0art0 Goto Github PK

automating-mathematics

categorytheory

Basic category theory in Lean4

cellular-automata

A collection of 2-D cellular automata simulations built on pygame.

chase

combinatornithology

A series of puzzles on combinatory logic written in LEAN, inspired by the book "To Mock a Mockingbird" by Raymond Smullyan.

dualnumbers

An implementation of dual numbers and polynomials in the Julia language. This includes an interactive Pluto notebook.

formal-systems

This repository contains implementations of various formal systems such as lambda calculus, SKI combinatory calculus and propositional logic.

freudenthal-hopf

Formalisation of the Freudenthal-Hopf theorem in Lean.

groupcomp

Lean 4 code and some slides for the NCM workshop on Groups and Computations at KREA, July 2023

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.

iiserp-sem5

A Links page for Semester V of IISER Pune in the 'Blessed' Year of 2020

iplug.github.io

IPLUG Website

jargoninator

A program that generates mathematical jargon by stringing together randomly chosen words according to the rules of grammar.

lambda-cube

A blog on mathematics, foundations, computer science and more.

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

Lean 4 programming language and theorem prover

lean4-gym

A REPL-like interface for Lean4 tactic proofs.

leandiscord-weekly

Weekly challenges for the Lean Discord Server.

leanink

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.

math-and-more

math-puzzles-in-lean4

math puzzles from various sources, formalized in Lean 4

pacman

This is a Pacman game.

polylean

proofwidgets4

Helper toolkit for creating your own Lean 4 UserWidgets

rewrite-system-interface

An implementation of rewrite systems in Lean together with a point-and-click interface for rewriting.

saturn

Experiments with SAT solvers with proofs in Lean 4

securemultipartycomputation

A repository hosting the code for the MTH329 Cryptography course group presentation.

sphere-eversion

Formalization of the existence of sphere eversions

std4

Standard Library for Lean 4