{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreiaolzpfp3ctmutpa7jmipi4wmpznrkmnfmpuvc6buzxdkw6kr7ndm",
    "uri": "at://did:plc:oygz2umq6txjgnjj7d72rfwu/app.bsky.feed.post/3mhbp276udrk2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreiethjouaejict7ceao2qrbfsy7a5kimgevgn7tuf56io5bzn2wygq"
    },
    "mimeType": "image/jpeg",
    "size": 135042
  },
  "path": "/news/20260317-leanstral-mistral/",
  "publishedAt": "2026-03-17T04:10:00.000Z",
  "site": "https://gigazine.net",
  "tags": [
    "AI,",
    "続きを読む..."
  ],
  "textContent": "フランスのAIスタートアップのMistral AIが、数学的証明やソフトウェア仕様の検証などを支援するAIモデル「Leanstral」を公開しました。Leanstralは形式証明ツール「Lean 4」に対応したオープンソースのAIエージェントで、数学やプログラムの正しさを厳密に検証する「証明エンジニアリング」を支援することを目的としています。\n\n**続きを読む...**",
  "title": "信頼できるAIコーディングを実現するためのオープンソース証明検証基盤「Leanstral」をMistral AIがリリース、重大なボトルネック「人間によるレビュー」の克服を目指す",
  "updatedAt": "2026-03-17T04:10:00.000Z"
}