This is your work, valued

Matěj Kripner

Expert
@Kripner

Automated/neural theorem proving, applied RL, robotics

nanoproof. Minimal open-source implementation of AlphaProof and HyperTree Proof Search.

86

openprover. Automated Theorem Prover inspired by Aletheia. Claude Code for mathematicians.

76

leantree. Structured data extraction and programmatic interaction with Lean 4.

20

goodseed. ML experiment tracker. Simple alternative for neptune.ai or Tensorboard.

18

textGenGen. MPS plugin for generating textGen definitions derived from editor definitions, so that the text generated by textGen is the same as the one rendered on the screen by the editor

9

lean-worlds. Combining symbolic model-based RL and formal mathematics language Lean.

7

mathemagician. A Flutter app for all people who love mental math.

3

ProofNet. Port of the ProofNet formal theorem proving benchmark to Lean 4.27.0

2

gym-cellular. Gym-based RL environments with dynamics driven by cellular automata.

1

Kripner.github.io. HTML

1

sian. Sian - Simple Animation Library

1

papiry. Python

1