Lean Programming Language
Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.
https://lean-lang.org/

Seed-Prover
Formal languages like Lean enable automatic verification, making them advantageous for reinforcement learning (RL) through Lemma-Style Proving: proving intermediate lemmas first → utilizing them for main theorems, and Iterative Refinement: iteratively improving proofs using Lean feedback, self-summarization, and leveraging previous proofs.
www.arxiv.org
https://www.arxiv.org/pdf/2507.23726

Seonglae Cho