Lean, 수학을 구원할까? 신뢰성 위기와 AI의 역습

Lean 커널에서 다시 soundness 버그를 보게 될까?

소프트웨어 개발자에게 이 질문은 미친 소리처럼 들린다. 과거에도 버그가 있었고, 앞으로도 분명 더 있을 것이다.

그런 버그를 보게 되면 AI Lean 증명에 어떤 의미가 있을까? 우리가 그것을 신뢰할 수 있을까?

이 모든 것은 결국 신뢰로 귀결된다.

우리는 인간의 검증을 높이 신뢰할 수 있는데, 그 이유는 커뮤니티와 평판, 그리고 인간의 proof-of-work 때문이다. 인간은 때때로 수학적 결과에 대해 거짓말을 하지만, 이런 이유로 그런 일은 드물다. 실수를 하면 그 실수는 대체로 신뢰할 만한 커뮤니티에 의해 발견된다.

LLM은 평판을 신경 쓰지 않는다. 자주 환각을 일으키고 조작한다. 하네스 안에서는 문자 그대로 속임수를 쓰고 규칙을 왜곡하려 하는데, 이는 규칙에 인코딩된 지식에 재앙이다. 그래서 우리는 증명 검사기에 의존할 수밖에 없다.

문제는 증명 검사기가 얼마나 신뢰할 만한가이다. 버그가 있는가? 그리고 기반 이론 자체가 역설과 불가해한 것들, 그리고 악용될 수 있는 수학적 "버그"로부터 자유로운가? 다른 수학자들을 속이려 작정한 인간 수학자를 상상해 보라. 검증기가 있더라도 우리가 그들의 돌파구를 신뢰할까?

이런 속성들 때문에 최후의 보루는 인간이어야 하며, 커뮤니티와 proof-of-work 기반의 인간 신뢰 시스템에 뿌리를 두어야 한다. 현재 사람들은 도구를 너무 많이 신뢰하고 있다.

예측: Navier-Stokes 증명에 의문을 제기하는 버그가 AI 도구를 사용하는 인간에 의해 발견될 것이다.