「なぜ？」から始まる、数学の冒険

小さな「なぜ？」。大きな冒険。

物語を追い、証明に触れる。気になったら、もうひとつ奥まで。

アカウント不要。APIキー不要。好奇心だけで。

ふたつの入口。お茶の間は、ひとつ。

まんがから入ります:17章、64個の小石、必須の式はゼロ。Leanの原文は、訪ねてくるまでガラス越しです。

証明マップから始めます:名付けられた定理が数千本。そして時計の逆元からR = Tまで、階段を全部登ります。となりでは物語も語り続け、あなたを正直に保ちます。

ふたりで読むために作りました:数学好きと、数学が苦手なひと。ソファは一台。それぞれが持ち帰ったものは、お茶の間へ運びます。

練習用のリアルタイム検査

小さな場面、本物の論理の目標。そして、あなたの成功を気にかけるハト。

theorem promise (P : Prop) : P → P := by
intro ticket
sorry

このページで物語と原文を読めます。証明の編集、クイズ、対話式のマップにはJavaScriptを有効にしてください。

練習用に作った試行です。試すと実際に検査されます。FLTの証明の歴史を再現したものではありません。

「これからもらうはずの切符を、先に堂々と提出します。」

exact ticket

ミカの手がかり

ticketはまだ手元にありません。intro ticketで前提Pの証拠を受け取り、その後で同じ証拠を返そう。

intro ticket
exact ticket