ABC予想の議論を呼ぶ証明をコンピュータソフトウェアを用いて検証しようとする取り組みが、進展を見せていない。「Lean and Anabelian Geometry（LANA）」プロジェクトの中間報告によると、数学者たちの間では、その根底にある理論の妥当性について依然として意見が分かれている。
2012年、京都大学の望月新一氏は、ABC予想に関する500ページに及ぶ証明を発表した。この証明は同氏が提唱する「宇宙際タイヒミューラー理論」に依拠しているが、これを検証できた数学者はごくわずかである。
LANAとして知られるプロジェクトは、プログラミング言語「Lean」を用いてこの証明の形式化を試みてきた。同プロジェクトの最近の中間報告によると、メンバー間で活発な議論が行われたものの、理論が成立するかどうかについて合意には至らなかった。
この報告書は、2018年にピーター・ショルツ氏とヤコブ・スティックス氏が提起した問題を浮き彫りにしている。ロンドン・クイーン・メアリー大学のアビシェク・サハ氏は、今回の結果は理論に重大な欠陥があるとする大半の数学者の見解と一致していると述べた。
ウエストレイク大学のイワン・フェセンコ氏は、こうした批判は的外れであり、最終的には形式化された証明が提示されるだろうと主張している。