테렌스 타오는 ‘Math 2.0’ 강연에서 AI로 대규모 수학 자료를 만들고 검증하는 연구 방향을 제시했다. 사례로 2200만 개 이상의 대수 명제를 판정한 Equational Theories Project와 24차 다항식의 2만5000개 갈루아 군을 찾는 협업을 들었다. Lean 같은 형식 검증, 살아 있는 논문 지식망, 정리의 가정을 바꿔 보는 실험도 활용 경로로 소개했다. 동시에 성공 사례뿐 아니라 계산 자원과 실패 결과를 공개해야 하며 대부분의 최전선 문제는 여전히 미해결이라고 강조했다. 자동 풀이의 증가를 수학 전체의 해결이나 인간의 이해와 동일시하지 않는 구상이다.