stringtranslate.com

Томас Каллистер Хейлс

Томас Каллистер Хейлз (родился 4 июня 1958 года) — американский математик, работающий в области теории представлений , дискретной геометрии и формальной верификации . В теории представлений он известен своей работой над программой Ленглендса и доказательством фундаментальной леммы над группой Sp(4) (многие из его идей были включены в окончательное доказательство фундаментальной леммы благодаря Нго Бао Чау ). В дискретной геометрии он подтвердил гипотезу Кеплера о плотности упаковок сфер , гипотезу о сотах и ​​гипотезу о додекаэдре . В 2014 году он объявил о завершении проекта Flyspeck, который формально подтвердил правильность его доказательства гипотезы Кеплера .

Биография

Он получил степень доктора философии в Принстонском университете в 1986 году, защитив диссертацию под названием «Субрегулярный росток орбитальных интегралов» . [1] [2] Хейлз преподавал в Гарвардском университете и Чикагском университете , [3] а с 1993 по 2002 год он работал в Мичиганском университете . [4]

В 1998 году Хейлз представил свою работу по компьютерному доказательству гипотезы Кеплера , многовековой проблемы дискретной геометрии , которая утверждает, что наиболее эффективным с точки зрения пространства способом упаковки сфер является форма тетраэдра. Ему помогал аспирант Сэмюэл Фергюсон. [5] В 1999 году Хейлз доказал гипотезу о сотах , а также заявил, что эта гипотеза могла быть в головах математиков до Марка Теренция Варрона . Гипотеза упоминается Паппом Александрийским в его Книге V.

После 2002 года Хейлз стал профессором математики в Университете Питтсбурга . В 2003 году Хейлз начал работу над Flyspeck, чтобы подтвердить свое доказательство гипотезы Кеплера. Его доказательство опиралось на компьютерные вычисления для проверки гипотез. В проекте использовались два помощника по доказательству , HOL Light и Isabelle . [6] [7] [8] [9] Annals of Mathematics приняли доказательство в 2005 году, но были уверены в нем только на 99%. [9] В августе 2014 года программное обеспечение команды Flyspeck наконец подтвердило правильность доказательства. [9]

В 2017 году он инициировал проект Formal Abstracts, целью которого является предоставление формализованных заявлений основных результатов каждой математической исследовательской работы на языке интерактивного доказательного устройства теорем . Цель этого проекта — извлечь выгоду из повышенной точности и совместимости, которые обеспечивает компьютерная формализация, избегая при этом усилий, которые в настоящее время влечет за собой полномасштабная формализация всех опубликованных доказательств. В долгосрочной перспективе проект надеется создать корпус математических фактов, который позволит применять методы машинного обучения в интерактивном и автоматизированном доказательстве теорем. [10]

Награды

Хейлз был приглашенным докладчиком на Международном конгрессе математиков в 2002 году. [11] Он выиграл премию Шовена в 2003 году, [12] премию Р. Э. Мура в 2004 году, [13] премию Лестера Р. Форда в 2008 году, [14] и премию Фулкерсона в 2009 году. [15] Он был награжден первой премией Роббинса Американского математического общества в 2007 году. [16] В 2012 году он стал членом Американского математического общества . [17] Он был приглашен прочитать лекции Тарского в 2019 году. Его три лекции назывались «Формальное доказательство гипотезы Кеплера», «Формализация математики» и «Интеграция с логикой». [18] [19] Он был награжден премией Старшего Бервика Лондонского математического общества в 2020 году. [20]

Публикации

Примечания

  1. ^ «Томас Хейлз — проект генеалогии математики».
  2. ^ Хейлз, Томас С. (1992). «Субрегулярный росток орбитальных интегралов» (PDF) . Мемуары Американского математического общества . 99 (476). doi :10.1090/MEMO/0476. S2CID  121175826. Архивировано из оригинала (PDF) 29.02.2020.
  3. ^ "Краткая биография Томаса С. Хейлза - thalespitt". Архивировано из оригинала 27.12.2020.
  4. ^ "Архивная копия". Архивировано из оригинала 2018-06-17 . Получено 2016-12-29 .{{cite web}}: CS1 maint: архивная копия как заголовок ( ссылка )
  5. ^ "Университет Питтсбурга: Кафедра математики". Архивировано из оригинала 2011-09-27 . Получено 2016-12-29 .
  6. ^ "Тейлспитт".
  7. ^ Проект Flyspeck
  8. ^ Хейлз решает старейшую задачу дискретной геометрии Архивировано 29 мая 2007 г. в Wayback Machine The University Record (Университет Мичигана), 16 сентября 1998 г.
  9. ^ abc Арон, Джейкоб (12 августа 2014 г.). «Подтверждено доказательство 400-летней проблемы укладки фруктов». New Scientist . Получено 10 мая 2017 г.
  10. ^ Сайт проекта https://formalabstracts.github.io/, получено 10.01.2020.
  11. ^ "ICM Plenary and Invited Speakers | Международный математический союз (IMU)". www.mathunion.org . Получено 2024-10-13 .
  12. ^ Хейлз, Томас С. (2000). «Пушечные ядра и соты». Уведомления AMS . 47 (4): 440–449.
  13. ^ "Томас С. Хейлз получает вторую премию имени Р. Э. Мура". www.reliable-computing.org . Получено 13 октября 2024 г.
  14. ^ Хейлз, Томас С. (2007). «Теорема о кривой Жордана, формально и неформально». American Mathematical Monthly . 114 (10): 882–894. doi :10.1080/00029890.2007.11920481. JSTOR  27642361. S2CID  887392.
  15. ^ "Просмотр призов и наград". Американское математическое общество . Получено 2024-10-13 .
  16. ^ "Просмотр призов и наград". Американское математическое общество . Получено 2024-10-13 .
  17. ↑ Список членов Американского математического общества, получен 19 января 2013 г.
  18. ^ "Лекции Тарского 2019 г. | Кафедра математики Калифорнийского университета в Беркли". math.berkeley.edu . Получено 2021-11-02 .
  19. ^ "Группа по логике и методологии науки - Лекции Тарского". logic.berkeley.edu . Получено 2021-11-02 .
  20. ^ "Победители премии LMS 2020 | Лондонское математическое общество". www.lms.ac.uk . Получено 13 октября 2024 г.

Внешние ссылки