Формальні системи доведення виявляють непомічені неоднозначності в передовій математиці

Таблиця посилань

Анотація

1. Подяки та вступ

2. Універсальні властивості

3. Добутки на практиці

4. Універсальні властивості в алгебраїчній геометрії

5. Проблема з використанням рівності Гротендіка

6. Більше про "канонічні" відображення

7. Канонічні ізоморфізми в більш просунутій математиці

8. Підсумок та посилання

Підсумок та посилання

Хоча я не стверджую про помилки в літературі чи прогалини в аргументах, які не можна заповнити після певної роботи, я доводжу, що ці прогалини існують, і що нова математика може знадобитися формалізаторам для ефективного заповнення цих прогалин. Прогалини бувають двох видів. По-перше, це проблема, коли люди створюють конструкції або доводять теореми, які суттєво використовують модель математичного об'єкта, визначеного з точністю до унікального ізоморфізму; прогалина полягає в тому, що потрібно перевірити, що аргумент не залежить від явних деталей моделі.

\ Математики добре усвідомлюють це, коли йдеться, наприклад, про вибір базису для векторного простору, а потім перевірку, що нічого важливого не залежало від вибору, або вибір представника для класу еквівалентності, а потім перевірку, що нічого важливого не залежить від представника. Однак вони, здається, менш обережні при виконанні більш просунутої математики, плутаючи "локалізацію" з "локалізацією" або "зворотне відображення" з "зворотним відображенням", і залишаючи читачеві деталі перевірки того, що багато діаграм комутують.

\ Один корисний трюк полягає в зловживанні символом рівності, змушуючи його означати те, чого він не означає; це може обманути читача, змушуючи думати, що нічого не потрібно перевіряти. Іноді такі перевірки можуть бути напрочуд болісними, і може бути легше реструктурувати математичний аргумент, ніж фактично робити ці перевірки. Другий вид прогалини - це проблема різних відображень (як граничні відображення в точних послідовностях), які розглядаються як "канонічні", хоча насправді вони не є унікальними, і робляться неявні вибори знаку.

\ На жаль, зовсім не складно вказати на явні приклади в літературі, де автор не вказує точно, яку конвенцію вони використовують, коли йдеться про такі речі, як теорія різноманітностей Шимури або гомологічна алгебра. Це створює непотрібний тягар для уважного математика (наприклад, Конрада або комп'ютерного доказувача теорем), який намагається використовувати або перевіряти роботу. Обидві ці проблеми проявилися в моїй роботі з формалізації, і я очікую, що вони будуть з'являтися частіше, коли ми глибше зануримося у формалізацію сучасної математики.

Посилання

[AX23] David Kurniadi Angdinata and Junyan Xu, An Elementary Formal Proof of the Group Law on Weierstrass Elliptic Curves in Any Characteristic, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2023, pp. 6:1– 6:19.

[BCM20] Kevin Buzzard, Johan Commelin, and Patrick Massot, Formalising perfectoid spaces, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020 (Jasmin Blanchette and Catalin Hritcu, eds.), ACM, 2020, pp. 299–312.

[BPL21] Anthony Bordg, Lawrence Paulson, and Wenda Li, Grothendieck's schemes in algebraic geometry, March 2021, https://isa-afp.org/entries/Grothendieck_Schemes.html, Formal proof development.

[Buz] Kevin M. Buzzard, Grothendieck's approach to equality, https://www.youtube.com/watch?v=-OjCMsqZ9ww, Accessed: 12-08-2023. [Buz19] Buzzard, Kevin, The inverse of a bijection, 2019, [Online; accessed 12-Aug-2023].

[Con00] Brian Conrad, Grothendieck duality and base change, Lecture Notes in Mathematics, vol. 1750, Springer-Verlag, Berlin, 2000. MR 1804902

[dFF23] Mar´ıa In´es de Frutos-Fern´andez, Formalizing Norm Extensions and Applications to Number Theory, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – LeibnizZentrum f¨ur Informatik, 2023, pp. 13:1–13:18.

[Gro60] A. Grothendieck, El´ements de g´eom´etrie alg´ebrique. I. Le langage des sch ´ ´emas, Inst. Hautes Etudes Sci. Publ. Math. (1960), no. 4, 228. MR 217083 ´

[Lan97] R. P. Langlands, Representations of abelian algebraic groups, Pacific J. Math. (1997), 231–250, Olga Taussky-Todd: in memoriam. MR 1610871

[Liv23] Amelia Livingston, Group Cohomology in the Lean Community Library, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2023, pp. 22:1–22:17.

[mC20] The mathlib Community, The lean mathematical library, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, jan 2020.

[Mil80] James S. Milne, Etale cohomology ´ , Princeton Mathematical Series, No. 33, Princeton University Press, Princeton, N.J., 1980. MR 559531

[Sta18] The Stacks Project Authors, Stacks Project, https://stacks.math.columbia.edu, 2018.

[Wei59] Andr´e Weil, Correspondence [signed "R. Lipschitz"], Ann. of Math. (2) 69 (1959), 247–251, Attributed to A. Weil. MR 100637 [Wik04a] Wikipedia contributors, Monoidal category — Wikipedia, the free encyclopedia, 2004, [Online; accessed 12-Aug-2023].

[Wik04b] , Ordered pair — Wikipedia, the free encyclopedia, 2004, [Online; accessed 20- May-2023].

[Zha23] Jujian Zhang, Formalising the Proj Construction in Lean, 14th International Conference on Interactive Theorem Proving (ITP 2023) (Dagstuhl, Germany) (Adam Naumowicz and Ren´e Thiemann, eds.), Leibniz International Proceedings in Informatics (LIPIcs), vol. 268, Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2023, pp. 35:1– 35:17.

[ZM23] Max Zeuner and Anders M¨ortberg, A univalent formalization of constructive affine schemes, 2023. Email address: [email protected] Department of Mathematics, Imperial College London

:::info Автор: KEVIN BUZZARD

:::

:::info Ця стаття доступна на arxiv за ліцензією CC BY 4.0 DEED.

:::

\