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

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

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

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

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

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

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

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

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

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

theorem duet (P Q : Prop) (singer : P) (pianist : Q) : P ∧ Q := by
sorry

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

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

「歌手を二回呼べば節約になる。数学的には、ちょっと怪しいけど。」

constructor
· exact singer
· exact singer

ミカの手がかり

Pの目標はもう閉じています。残るQにはpianistが必要です。singerはPの証拠なので、もう一方の証拠にはなりません。

constructor
· exact singer
· exact pianist