---
name: Mathlib v4.27 API 注意点リスト
description: 2026-04-21 STEP 950-967 ビルド検証で判明した Mathlib v4.27 の API 不在・変更項目
type: feedback
originSessionId: 80a567c3-c92a-4757-ac12-f814a062c754
---
Mathlib v4.27 (現在の lean-toolchain) で頻出するビルドエラーパターン:

| 古い API | 現行 (v4.27) | 備考 |
|---------|--------------|------|
| `List.bind` | `List.flatMap` | v4.27 で削除済み |
| `Nat.popcount` | (Mathlib に無し) | 自前で `Nat.bits.count` 等で実装 |
| `Nat.factors` | (削除/移動) | `Nat.primeFactorsList` を検討 |
| `Submodule.isPrincipal` | (パス変更) | namespace を確認 |
| `Mathlib.NumberTheory.ArithmeticFunction` (一括) | 個別 import 推奨 | `Defs/Misc/Moebius/VonMangoldt/Zeta` に分割 |
| `Mathlib.GroupTheory.Basic` | (olean 不在の可能性) | 上位の `Mathlib.Algebra.Group.Defs` 等を検討 |

**Real 関数の noncomputable:**
- `Real.exp`, `Real.log`, `Real.sqrt` 等は noncomputable
- これらを使う `def` は `noncomputable def` で宣言する必要あり
- そうしないと "failed to compile definition, depends on 'Real.instDivInvMonoid' which is noncomputable" エラー

**parse error の典型:**
- `theorem foo : ... := by tactic /-- next docstring -/` の形は parse error
- docstring と前の theorem の間に空行を入れる

**native_decide が false を返すケース:**
- 自分が書いた witness が実際には条件を満たしていない数学的バグ
- まず小規模で手計算検証してから native_decide で確認

**Why:** 2026-04-21 の STEP 950-967 ビルド検証で 14 ファイルがこれらのエラーで破綻。原因はほぼ全て Mathlib バージョン差と API 知識不足。

**How to apply:** 新規 Lean ファイルで上記 API を使う前に、まず `lake env lean -e "import Mathlib; #check List.bind"` 等で存在確認するか、Mathlib4 docs (https://leanprover-community.github.io/mathlib4_docs/) で検索。