ケプラー予想の証明の概略は下記プレプリントに出ています（査読後出版済み）。
https://arxiv.org/pdf/1501.02155.pdf
証明支援システムは使ったことがないのでわかりませんが、jupyterやgoogle colaboratoryのような、打ち込んで実行した結果が記録されるノート形式の実行環境ではないかと思います。証明は164000行のそういうコードからなるということで、数人のチームで完成に10年かかった、というのは納得できます。上記論文の中には記号論理学で使う記号がたくさん使われています。私は大学1年生のときにゲーデルの不完全性定理を知りたくて記号論理学を履修しましたが、難しくて、一行ごとになんでそんなことをするのか理解するのに骨がおれました。いまは周辺知識が増えているのでだいぶ楽です。とくに、コンピュータとのつながりが面白いと思います。Haskelという（私には難解な）コンピュータ言語がありますが、その名前の元になっているProf. Haskel Curryのパラドックスなどは面白いです。
https://ja.wikipedia.org/wiki/%E3%83%8F%E3%82%B9%E3%82%B1%E3%83%AB%E3%83%BB%E3%82%AB%E3%83%AA%E3%83%BC
Yahoo知恵袋は間違いが多いですが、下記は大丈夫ではないかと思います。
https://detail.chiebukuro.yahoo.co.jp/qa/question_detail/q1158859171
Curryのパラドックスは「この文が正しければ、ドラえもんは実在する」が論理的（自然演繹論理）には真になってしまうというパラドックスです。
わかりにくいですが、「この文が正しい」と仮定すると、「ドラえもんは実在する」ことになり、つまり「この文が正しい」ことになるということです。
似たような「嘘つきパラドックス」とは「私は嘘つきです」を真としても偽としても矛盾が生じるというパラドックスです。どちらも自己言及文であるところが問題です。wikipedia日本版によると、嘘つきパラドックスを除去する規則は作れるが、Curryのパラドックスは除去しにくいそうです。英語版には「論理学者たちの結論はでていない」に対応する文はないようです。
https://ja.wikipedia.org/wiki/%E3%82%AB%E3%83%AA%E3%83%BC%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9
英語は、 https://en.wikipedia.org/wiki/Curry%27s_paradox から
curry 食べ物のカレー
Curry 食べ物とは関係なく、アイルランド系の苗字。日本語ではカリーと書くことが多い。
“Curry’s paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself “If C, then F”, requiring only a few apparently innocuous logical deduction rules. ”
arbitrary アー「ビ」トラリ 任意の
claim 主張、クレーム
from the mere existence 存在だけで
apparently innocuous 見かけ上差しさわりのない
innocuous イ「ノ」キュアス 無害な
logical deduction rules 論理的演繹規則 ディダクション
deduce ディ「デュ」ース 演繹する
induce イン「デュ」ース 帰納する 引き起こす
induction 帰納する、（電磁）誘導する
inductance インダクタンス（電気工学で、コイルのこと、コイルの値、単位はヘンリーH）
conditional 条件文の
Gödel’s incompleteness theorems ゲーデルの不完全性定理（いくつかある）
axiom 公理
“His conclusion may be stated as saying that combinatory logic and lambda calculus cannot be made consistent as deductive languages, while still allowing recursion.”
combinatory コンビナトリ 訳さずとそのまま使うようです。
lambda calculus ラムダ算法
recursion 回帰
※この辺の追究からHaskel言語が生まれたのでしょう。