Террі Тао опублікував пост про автоформалізацію математики за допомогою ШІ у системі Lean
What mathematicians should know about the Lean Theorem Prover: reliability & AI
У гостьовому пості в блозі математика Террі Тао дослідник Томас Хейлс розповідає про стан автоформалізації математики — перетворення паперових доведень на формальні докази, перевірені комп'ютером, зокрема в системі Lean. За його словами, у 2026 році автоформалізація великими мовними моделями стала практичною реальністю: Anthropic формалізувала Велику теорему ферма за 11 днів, а OpenAI — теорему про сплеск Нав'є-Стокса. Автор також пояснює засади надійності Lean і роль бібліотеки mathlib, яка містить майже 300 тисяч теорем.
Мовою оригіналу · EN
Guest post on Terry Tao's blog: autoformalization of mathematics via LLMs and the Lean prover became practical reality in 2026.
Читати оригінал на Hacker News (100+ балів) →
Чому в стрічці: Технічний огляд конкретних досягнень AI у формалізації математики, що відповідає інтересу до AI-технологій.