- Terence Tao의 mathstodon.xyz 게시글
- Terence Tao의 최근 논문에서 Lean4 형식화 프로젝트로 인한 작지만 중요한 버그 발견
- 논문 6페이지에서 형식화하는 과정에서 버그 발견, 논문은 https://arxiv.org/pdf/2310.05328.pdf에서 확인 가능
- Tao의 논문에서 n=3, k=2인 경우에 발산하…
잼난 개발놀이, 노리컴퍼니