ProofTrace は「問題を解くアプリ」ではありません。
正しい証明の書き方を教えたり、解答を生成したり、速さや効率を最適化したりもしません。
ProofTrace は、証明を“完成した文章”としてではなく、“たどれる思考の過程”として残すための学習支援ツールです。
私たちは証明を「書く」のではなく、「追跡（trace）する」。
何ができる？
ProofTrace では、理解の途中経過を Proof Trace（証明トレース）として記録します。
トレースは、未完成・誤り・試行錯誤・放棄を含んでかまいません。むしろそれらが中心です。
ユーザーが残すのは、たとえばこんな情報です。
- なぜその方針を選んだのか
- どこで行き詰まったのか（失敗の記録）
- どんな代案を考えたのか
- 定義・定理・仮定をどう使った（つもり）なのか
こんな人へ
- 大学数学の「証明が読めない／追えない」を越えたい学部生
- 証明の“構造”が見えずに苦しんでいる大学院生・自習者
- 数学・CS・論理の読書会や個別指導で、思考のログを残したい人
ProofTrace が目指すもの
ProofTrace が助けたいのは、次のようなことです。
- 証明が「どこへ向かっているか」を見失わない
- なぜその戦略が効く（あるいは効かない）のかを言語化する
- 文章のうまさよりも 構造を掴む
- 理解した型（パターン）を、次の証明へ持ち越す
使い方の流れ（ざっくり）
- 新しい Proof Trace を作成：定理名やタイトル、任意で文脈（教科書名など）だけで開始できます。
- 最初の一歩は未整理でOK：「この証明は何をしたい？」「関係しそうな定義は？」「何がわからない？」を書きます。
- Step を追加：サブゴール、見込み、疑問、参照（定義・定理・仮定）などを断片として積みます。
- 並べ替え・差し込み：順番が前後してもよく、途中に「穴」を開けてもかまいません。
- 失敗を残す：うまくいかなかった方針は、消さずに Failure として保存します。
- 中断して戻る：完成要求はありません。やめたところから再開できます。
コア機能（MVP）
- Proof Trace の作成（タイトル＋任意の文脈）
- Step の追加・編集（自由記述／参照タグ／不確かさの印）
- Step の並べ替え・再構成（非線形な理解を前提）
- Failure（失敗）を“消さずに”明示的に記録
- 未完成のまま保存（完了条件なし）
- 過去トレースの閲覧（達成度やスコアは出さない）
- ローカル保存（MVPは local-first）
やらないこと（Non-Goals）
ProofTrace は意図的に、次のことをしません。これらは「未実装」ではなく「設計判断」です。
- 問題を解く／解法へ誘導する
- 証明（部分証明やアウトライン含む）を自動生成する
- 正しさ判定・採点・評価をする
- ゲーミフィケーション（レベル、実績、スコア等）
- 「完了」状態を作る／完了を促す
- 教科書的な解説・講義コンテンツを提供する
用語（最小）
- Proof Trace：証明を理解しようとする試みの、構造化された記録。完成物ではありません。
- Step：推論の単位。仮の主張、サブゴール、疑問、参照など何でも入ります。
- Failure：うまくいかなかったアプローチを示す Step。消さずに残します。
- Uncertainty：確信がないことを明示する印。未解決でもかまいません。
- Margins（マージン）：証明の「本文」から外れた周辺情報の置き場。たとえば、思いつき・メモ・比喩・関連する定理の候補・直感・反例案・疑い・後で調べることなど、いま本文に入れるには粗いが将来の理解に効く“余白”を保存します（本文の邪魔をせず、思考の痕跡を残すための領域）。
Proofs are not written here. They are traced.