Daniel Selsam

certigrad. Bug-free machine learning on stochastic computation graphs

neurosat. NeuroSAT: Learning a SAT Solver from Single-Bit Supervision

neurocore-public. NeuroCore: Guiding CDCL with Unsat-Core Predictions

tc. Reference type checker for the Lean theorem prover

lean-python-bindings. Python Bindings to the Lean Theorem Prover http://leanprover.github.io/

lean-gym. Lean

binport. A tool for building Lean4 .olean files from Lean3 export data

neurocuber. NeuroCuber: training NeuroSAT to make cubing decisions for hard SAT problems

terpret_problem. A simple demonstration of the "Terpret" problem, in which gradient descent fails.

arc. Experimental solver for ARC

islanders. Formalization of the infamous blue-eyed islanders puzzle in Lean.

larc. Neuro-Symbolic ARC Solver in Lean4

oracle. Haskell prototype of the Search Transformer and Universal Oracle

lean. Lean Theorem Prover

search. Search transformers for Lean4

lean-step-public. Proof artifact co-training for Lean

mathzoo. Lean mathzoo

nnsos. Synthetic data for (cyclic) sum-of-squares decomposition problems.

minGPT. A minimal PyTorch re-implementation of the OpenAI GPT (Generative Pretrained Transformer) training

minisat. A minimalistic and high-performance SAT solver

cs103. Lean

lean4. Lean4 work in progress repo

identity. Training an MLP on the identity function.