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

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

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

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

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

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

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

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

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

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

theorem impossible_guest (P : Prop) (guest : P) (rule : P → False) : False := by
sorry

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

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

「ありえなさそうな来客なので、そのままFalseの棚へ入れます。」

exact guest

ミカの手がかり

guestはPの証拠で、Falseの証拠ではありません。ruleがPからFalseを導きます。rule guestで二つの仮定の矛盾を取り出そう。

exact rule guest