Cajal
Winter 2026活動中formal verificationをスケールさせ、科学的発見を加速
- サマリー
- 量子コンピューティングや金融分野向けに、AI数学者による形式検証を提供する
- 課題
- AIが発見した数学的手法の正しさを検証し、科学研究に活用するのが難しい
- 解決策
- Leanで数学的主張を形式検証し、AI数学者を大規模展開して発見を加速する
AI による要約
- 所在地
- San Francisco, CA, USA
- チーム規模
- 2 人
事業内容
Cajal（YC W26）は、formal verificationを大規模に展開し、科学的発見を加速する。まずは量子コンピューティングと金融を対象に、影響力の大きい応用分野へ超人的なAI数学者を投入する。 Leanを使うことで、あらゆる数学的命題を形式検証できる。これによりAIを真理に根付かせ、システムが発見したツールを検証する。