Conjectura ABC

Uma disputa de uma década em matemática sobre a prova da conjectura ABC de Shinichi Mochizuki pode ser resolvida usando formalização computacional. Mochizuki sugeriu traduzir seu trabalho de 500 páginas para a linguagem de programação Lean para verificação automatizada. Essa abordagem poderia unir divisões entre campos conflitantes na comunidade matemática.