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

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

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

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

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

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

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

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

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

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

theorem cross_bridge (P Q : Prop) (bridge : P → Q) (ticket : P) : Q := by
apply bridge
sorry

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

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

「橋を丸ごと提出。これで渡ったことになるでしょう。」

exact bridge

ミカの手がかり

bridgeの型はP→Qですが、目標はQです。Pの証拠ticketを橋に渡すと、bridge ticketの型がQになります。

exact bridge ticket