mirefek

geo_logic. Tool for euclidean geometry aware of logic

lean-tactic-programming-guide. Beginner's guide to Tactic Programming in Lean

sokoban.lean. Sokoban implementation in lean for proving solvability / unsolvability

py_euclidea. Python version of the Euclidea game for possible reinforcement learning agents

HolStep-Tree. Python

HexProver. interactve prover of Hex diagrams

pyggb. Python tool for generating pictures from geometric constructions

manim. Animation engine for explanatory math videos

neur-rec-seq. Experimental neural architecture for self-repetitive (recursively defined) sequences

my-lean-experiments. Lean