Hacker News 의견

• 대학원 시절에 빠른 코드를 작성하여 Birch와 Swinnerton-Dyer 추측을 돕던 경험을 회상함. 세미나에서 반례를 찾고 싶다고 말했을 때 전문가들이 화를 냈음. 수학의 깊이를 이해하지 못했지만, 호기심을 자극받았음.

• 수학의 형식주의 발전에 기쁨을 느낌. 프로그래머로서 수학을 더 접근하기 쉽게 만듦. 형식주의 부족에 대한 불안은 호기심으로 대처해야 함.

• 수학자들이 자주 세부사항을 생략하는 경향이 있음. 엄격한 증명을 원하면 전문가의 도움이 필요함. 현대 수학은 불안정한 기반 위에 있음.

• 앤드류 와일즈가 FLT를 증명하는 과정을 회상함. 1990년대의 증명 방식이 오래된 것처럼 느껴짐.

• 현대 수학의 문서화가 부족함을 강조함. 형식 시스템을 통해 오류를 줄일 필요가 있음. 기계에게 수학적 논증을 가르치는 것이 중요함.

• UI/UX 디자이너와 개발자의 역할 차이를 설명함. 디자인과 개발은 다른 사고방식을 요구함.

• Lean과 같은 정리 증명기가 수학에서 중요한 도구가 될 것임을 기대함.

• Lean 코드를 살펴보는 것이 흥미로움. 최종 증명문이 유닛 테스트 역할을 함.

• 수십 년간 사용된 수학적 개념이 잘못되었을 가능성에 대한 의문을 제기함.

• 'vitiated'라는 단어를 소개하며, 증명이 잘못되었을 때 사용하기 좋다고 언급함.

• 수학자와 엔지니어 간의 격차를 언급하며, 기계가 수학을 해결할 때도 성능 향상이 필요할 것임을 기대함.

• 수학 문헌의 상태에 실망감을 표함. 1960년대부터 1990년대까지의 수론 문헌에 문제가 있을 것으로 예상함. 전문가 커뮤니티가 작을수록 오류가 쉽게 간과될 수 있음.