Formal LabMathematics ⇄ Lean
参照

Navigate the formal text

章・問題・解答・用語・文献を横断検索

検索語を入力してください。

    ↑↓ で移動、Enter で開く、Esc で閉じます。

    用語・記法・文献を一覧から探す

    Evidence, scope, and limits

    本書は何を、どこまで検査しているか

    正しさ、説明、学習活動、生成物、操作性は、同じ一つの点数では測れません。本書では要求ごとに証拠を分け、未観察を成功に数えずに公開します。

    現在の判定ゲート適合・未観察事項あり実証可能な学術教科書品質標準 0.1.0・Formal Lab 教科書・静的公開プロファイル 0.1.0

    Evidence snapshot

    検査された範囲

    件数は品質の得点ではなく、どこまで証拠が届いているかを示す分母付きの範囲です。

    79/79
    全基準を査読した章
    948/948
    証拠へ接続した品質主張
    79/79
    証拠へ接続した章の要点237件の個別証拠
    268/268
    練習へ接続した到達能力
    268/268
    評価へ接続した到達能力
    35/35
    ブラウザで検査するUI条件

    Non-compensatory review

    章ごとの品質査読

    重大な欠陥を他項目の高得点で相殺しません。各章は内容hashで改訂を固定し、十二の観点をそれぞれ証拠付きで査読します。

    観点種別範囲証拠
    主張の追跡可能性ゲート79章中、合格79章、改訂要0章、未査読0章形式証明・出典・人手査読
    適用範囲の明示ゲート79章中、合格79章、改訂要0章、未査読0章人手査読
    前提の先行ゲート79章中、合格79章、改訂要0章、未査読0章人手査読
    必要最小限の依存診断79章中、合格79章、改訂要0章、未査読0章人手査読
    定義を必要にする説明診断79章中、合格79章、改訂要0章、未査読0章人手査読
    例・非例・最初の使用診断79章中、合格79章、改訂要0章、未査読0章完成例・人手査読
    表現間の往復ゲート79章中、合格79章、改訂要0章、未査読0章完成例・人手査読
    到達目標・活動・評価の整合ゲート79章中、合格79章、改訂要0章、未査読0章人手査読
    補助を減らす練習系列診断79章中、合格79章、改訂要0章、未査読0章完成例・人手査読
    歴史的主張の文献的根拠ゲート79章中、合格79章、改訂要0章、未査読0章出典
    検査可能な成果物ゲート79章中、合格79章、改訂要0章、未査読0章自動検査
    発見可能性と局所的一貫性診断79章中、合格79章、改訂要0章、未査読0章人手査読

    Publication contracts

    公開物としての検査

    本文の査読と、ウェブ生成物の再現性・転送量・操作性を別の契約として検査します。

    静的サイトの全生成物

    決定的な公開物

    固定した入力から静的公開物を二回生成し、全通常ファイルの経路、容量、内容を一致させる。

    固定したNode・pnpm・Lean環境で二回の静的生成物を内容hashまで比較する。
    • scripts/check-build-reproducibility.ts — 成果物木の経路・容量・SHA-256比較
    • .github/workflows/ci.yml — 空のCI環境から同じ工程を実行

    HTML、CSS、JavaScript、検索DB、Lean原典

    配布性能予算

    初期読書面、遅延検索、個別ページ、配布物総量に独立した容量上限を適用する。

    9個の独立した容量予算を生成物へ適用する。
    • scripts/check-site-budgets.ts — raw・gzip・Brotli容量の上限検査
    • authoring/assurance/site-budgets.ts — 予算値と対象asset群

    主要公開面と代表章

    主要な読書経路

    章の選択、本文とLeanの照合、検索、問題、表示条件、失敗時経路を実配信面で検査する。

    35条件中35条件を、実ブラウザで検査する。
    • tests/e2e/ — 35件のブラウザ観察
    • src/site/assurance.ts — 読者タスクと表示条件の対応

    機械可読な適合性レポート（JSON）には、標準版、プロファイル、改訂hash、要求、観察、証拠位置、限界を収録しています。

    Claims not made

    この判定が意味しないこと

    証拠のない広い主張を避けるため、未観察事項とその帰結を判定本体に残します。

    学習成果

    268能力について練習と評価の整合を検査したが、実読者の遂行観察は0件である。

    本レポートは、個々の読者が能力を獲得したことを主張しない。

    アクセシビリティ

    自動監査とブラウザ操作は、実支援技術による意味上の読みやすさを代替しない。

    WCAG 2.2全体への適合や、数式の読み上げ品質を主張しない。

    外部資料

    外部URLは公開前監査の時点後に変更または停止し得る。

    ネットワーク監査を決定的ビルドとは分離し、公開前に再実行する。

    Reproduce the evidence

    同じ検査を再実行する

    固定したNode、pnpm、Leanとlockfileから、次の工程を実行できます。外部リンクだけはネットワーク状態に依存するため、決定的な検証とは分けています。

    pnpm install --frozen-lockfile
pnpm run verify
pnpm run audit:external
    証拠改訂
    sha256:ceb8cab2877f0d0bc673cddb18a4fac2588f752ebb0a7cf19c3f91050275a262
    査読更新日
    2026-08-09
    Node / pnpm
    26.7.0 / 11.20.0
    Lean / mathlib
    4.32.2 / v4.32.2
    読者遂行の観察
    0件
    UIの人手観察
    0件