Matěj Kripner

automated theorem proving (@leanprover), robotics, and applied RL

advised by @straka_milan and @lifrordi

[Matěj Kripner @MatejKripner]

I'm releasing nanoproof - a minimal open-source implementation of AlphaProof (@TZahavy). It uses nanochat (@karpathy) for pretrain+midtrain+sft, and the official AlphaProof pseudocode for MCTS+the RL loop. First version has 32.8% on minif2f with ~0.001% of the compute. (link to repo below)

[Matěj Kripner @MatejKripner]

Try it out: https://t.co/ecyMqO5XqY

paper: https://t.co/RiRItwq1AL

[Matěj Kripner @MatejKripner]

Our group around @VaclavRozhon and @AdrianZamecnik created Bolzano, a multi-agent AI system that produced new results on 7 problems in cryptography, combinatorics, and theoretical CS.

Five are publishable research results; four were produced essentially autonomously.

Have a hard problem to solve? Bolzano is now publicly available.

[Matěj Kripner @MatejKripner]

Using the significance-autonomy taxonomy introduced by @tonylfeng @lmthang, our results confirm that AI can contribute meaningfully to mathematical research, complementing reports by e.g. @SebastienBubeck and @mirrokni

[Matěj Kripner @MatejKripner]

Try it to train your own agent:

```
docker pull https://t.co/PjvfQ4ahSP

docker run --rm --gpus all https://t.co/PjvfQ4ahSP \
python scripts/reinforcement_learning/rsl_rl/train.py \
--task Isaac-Lift-Cube-Franka-v0 \
--num_envs 4096 --headless presets=newton
```

[Matěj Kripner @MatejKripner]

The Isaac Lab+Newton stack by @NVIDIARobotics is out and exciting, but still a bit rough to install and use, and there's no official container yet.

To work around this, I'm releasing a plug-and-play container based on my fork of Isaac Lab:

https://t.co/PjvfQ4ahSP

[Matěj Kripner @MatejKripner]

Other rough edges smoothed in the fork:

- randomize_rigid_body_material crashed on Newton (PhysX-only API) -> now skipped with a warning
(will soon be resolved by https://t.co/5RCO7RwjyQ)
- A pyglet 3.0 pre-release was breaking `https://t.co/gxIwqkC51h -i` -> pinned to <3.0

[Matěj Kripner @MatejKripner]

@jjoshua2 @MistralAI Will do, sorry about the delay

[Matěj Kripner @MatejKripner]

Leanstral by @MistralAI is now available in OpenProver!

openprover theorem.md --model=leanstral

[Matěj Kripner @MatejKripner]

I'm releasing OpenProver v1.0.0!

It's 1) an open-source automated theorem prover inspired by DeepMind's Aletheia (@tonylfeng @gjb_ai @lmthang), and 2) a "Claude Code for mathematicians", allowing interactive proof search in English and formalization in Lean.

[Matěj Kripner @MatejKripner]

@lmthang @tonylfeng @gjb_ai Thank you!

[Matěj Kripner @MatejKripner]

I'm releasing OpenProver v1.0.0!

It's 1) an open-source automated theorem prover inspired by DeepMind's Aletheia (@tonylfeng @gjb_ai @lmthang), and 2) a "Claude Code for mathematicians", allowing interactive proof search in English and formalization in Lean.

[Matěj Kripner @MatejKripner]

@JasonRute Thank you, will try that tomorrow!

[Matěj Kripner @MatejKripner]

You can try OpenProver today or fork it for your own project!

repo: https://t.co/Ty6zbe3dnS
pip install openprover

Also, if you'd like to sponsor OpenProver evaluation using a specific underlying model, get in touch!

[Matěj Kripner @MatejKripner]

2) Claude Code for Mathematicians

In interactive mode, OpenProver first searches for a proof in natural language. Then, if Lean formalization of the theorem is provided, it attempts to give a formal proof. OpenProver can also run in a formalization-only mode.