الباحثون

Matěj Kripner

المنشورات 2

نسخة أولية وصول مفتوح

NanoProof: Open and Efficient Automated Theorem Proving in Lean 4

Matěj Kripner, Milan Straka · 2026

We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof …

نسخة أولية وصول مفتوح

From Expert-Guided Proof Search to Automated Open-Problem Solving

Adrián Zámečník, Matěj Kripner, Martin Koutecký وآخرون · 2026

Large language models are increasingly contributing to mathematical research, where progress often depends on efficient proof search, incremental improvements and careful verification. We describe Bolzano, a multi-agent open-source system that uses parallel prover agents with a verifier agent and maintains a human-read …

المؤلفون المشاركون