Update: Mochizuki's ABC Conjecture proof is unformalizable

Here's the report: https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...