テクノロジー
Robinhood CEO率いるHarmonicが14.5億ドルの評価額で資金調達：数学的推論で目指すAIの「確率」から「証明」への道
米株式取引アプリ大手RobinhoodのCEO、Vlad Tenev氏が共同設立したAIスタートアップ「Harmonic」が、シリーズCラウンドにおいて1億2000万ドル（約180億円）の資金調達を完了し、その企業評価額 […]
Term
Lean 4
別名: Lean
Overview
最終更新: 2026年7月9日Microsoft Researchなどで開発された、定理証明支援系およびプログラミング言語。数学的な推論を厳密な形式で記述でき、その論理的な正しさをコンピュータが自動的に検証（形式検証）できる。HarmonicのAIモデル「Aristotle」の推論エンジンとして採用されており、AIが生成した回答が数学的に正しいことを保証するための基盤となっている。
Mentioned Articles
1 件External Mentions
10 件- arXivAn Agentic Formalization for Certified Quantum Neural Network Design
- arXivEvidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
- arXivSuperlinear complexity of the $(3/2)^n$ steering word
- arXivTreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
- arXivAn Overlap Construction for Relative Linear Extension Ratios
- arXivFrom Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game
- arXivCantor measures with odd base do not admit Fourier frames
- arXivMinimum modulus for the unique multiset-sum problem
- arXivStable Phase Retrieval for Spans of Independent Random Variables
- arXivAxioms for physical reasoning: codifying the Seiberg--Witten solution in Lean