Jason Rute

puzzle_cube. Solving the Rubik's cube with deep reinforcement learning and Monte Carlo tree search

modulize. A Python decorator for converting a function into a module. It also includes tools for combining multiple Python files into one.

lean_proof_recording. Proof recording for Lean 3

thoughts-on-ai-for-theorem-proving.

csb_neural_network. Training a neural network to compete in the Coder's Strike Back competition on CodinGame.com

holist-communication-example. Example communicating with HOList

communicating-with-lean. Prototype of back-and-forth tactic application in Lean through an external program.

lean-proof-recording-public-old. Recording of tactic proofs in Lean 3 for machine learning

Neural-Network. An implementation of a neural network in pure Python/NumPy. Useful for programming competitions.

puzzle_cube_code. Code submodule for the Rubik's cube project

lean_gym_prototype. A prototype version of a machine learning gym for the Lean 3 theorem prover

annotated_lean. Annotated lean files

lean_data_structures. Purely functional data structures in Lean

lean_info_scrapper. Scrapes all info messages from all lean files (both system and mathlib)

codingame_arena. An arena for CodinGame games. (Currently works for only Wonder Women.)

CG-Tron-Simulator. A simulator for the Tron multiplayer competition on CodinGame.com