Формальные системы доказательств выявляют упущенные неоднозначности в продвинутой математике

Таблица ссылок

Аннотация

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.

:::

\