2026-05-31
2026-05-30←前　次→2026-06-01
Leanが使用されている事例
分散システム検証
Veil
実運用寄り
AlphaProof
Google DeepMind
Lean上で数学証明を生成
IMO銀メダル級問題を解く
Leanで証明を生成
AlphaZero系探索＋LLM
Cedar
AWSの認可ポリシー言語
verification-guided development
Leanモデル + Rust実装差分テスト
LNSym
AWS系
暗号プロトコル向けシンボリック実行
How the Lean language brings math to coding and coding to math - Amazon Science. 2024-08-16
GitHub: leanprover/LNSym: Armv8 Native Code Symbolic Simulator in Lean
SampCert
サンプリングアルゴリズム検証
GitHub: leanprover/SampCert: SampCert : Verified Differential Privacy
【2004.00010】 The Discrete Gaussian for Differential Privacy
AILean
Rust検証
Aeneas
Rust → Lean変換
borrow semanticsを純関数化
Hax
Rust → Lean / Coq / F*
暗号ライブラリ検証で利用
分散システム
Veil
Paxos
Raft系
分散合意プロトコル検証のマルチモーダル検証(?)
Veil: Multi-Modal Verification of Distributed Protocols — Lean Lang
マルチモーダル検証 Loom: verse-lab/loom: Loom is a framework for automated generation of foundational multi-modal verifiers.
Lean-SMT: ufmg-smite/lean-smt: Tactics for discharging Lean goals into SMT solvers.
暗号・zkVM
RISC Zero zkVM
zkVM(ゼロ知識仮想マシン、、zero-knowledge Virtual Machine)仕様のLeanモデル
zkVM とは何か｜zkVM 簡易解説
ゼロ知識証明を知りたい人のためのzkVM作成入門
risc0/risc0-lean4: A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover
Ethereum Foundation zkEVM Verification Project
Lean + Aeneas/Hax + AI prover
Merkle証明
FRI
多項式評価(Polynomial evaluation)
【2605.30106】 A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
OS
seLe4n
Lean 4製マイクロカーネル
seL4を意識
公式: seLe4n — A Microkernel Written in Lean 4
GitHub: hatter6822/seLe4n: A capability-based microkernel written in Lean 4
コンパイラ
Axon Verified Compiler
Leanでコンパイラ実装と正当性証明
Claude Codeが大量生成
arXiv: Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
LeanおよびClaude Codeを用いたAxon検証済みコンパイラにおける、テスト、信頼できるコンパイル、および検証 | alphaXiv
Lean自己検証
Lean4Lean
Leanの型検査器をLeanで実装
self-hosting verification
機械学習
TorchLean
ニューラルネットワーク形式化
プロジェクトサイト: TorchLean | Lean 4 tools for neural-network semantics, runtime experiments, and verification.
LeanDojo
傾向
Rust普及により
Rust
↓
Lean
↓
機能正当性証明
という流れが強くなっている
#日誌