Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Autor: Baanen, Anne, Best, Alex J., Coppola, Nirvana, Dahmen, Sander R., Krebbers, Robbert, Traytel, Dmitriy, Pientka, Brigitte, Zdancewic, Steve

Publikováno v: CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023, 47-62
STARTPAGE=47;ENDPAGE=62;TITLE=CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023
Baanen, A, Best, A J, Coppola, N & Dahmen, S R 2023, Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves . in R Krebbers, D Traytel, B Pientka & S Zdancewic (eds), CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023 . Association for Computing Machinery, Inc, pp. 47-62, 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023-Co-located with POPL 2023, Boston, United States, 16/01/23 . https://doi.org/10.1145/3573105.3575682

Diophantine equations are a popular and active area of research in number theory. In this paper we consider Mordell equations, which are of the form $y^2=x^3+d$, where $d$ is a (given) nonzero integer number and all solutions in integers $x$ and $y$

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::881c967c1d4906a7bc1c6de0f2b6a8e6
http://arxiv.org/abs/2209.15492

Formalizing Geometric Algebra in Lean

Autor: Wieser, E, Song, U

This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon the substantial body of work that is the Lean mathematics library, mathlib. As we use Lean source code to demonstrate many of our ideas, we

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6645965f6830ae43b93d413cbbf95924
https://www.repository.cam.ac.uk/handle/1810/336169

Formalizing the Ring of Adèles of a Global Field

Autor: de Frutos-Fernández, María Inés

The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalized adic v

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8ebc46e189500e2998d1fa179f67ba06

A Formalization of Dedekind Domains and Class Groups of Global Fields

Autor: Baanen, Anne, Dahmen, Sander R., Narayanan, Ashvni, Di Capriglio, Filippo A.E.Nuccio Mortarino Majno, Cohen, Liron, Kaliszyk, Cezary

Publikováno v: 12th International Conference on Interactive Theorem Proving (ITP 2021)
12th International Conference on Interactive Theorem Proving (ITP 2021), Jun 2021, Rome, Italy. ⟨10.4230/LIPIcs.ITP.2021.5⟩
Baanen, A, Dahmen, S R, Narayanan, A & Di Capriglio, F A E N M M 2021, A formalization of Dedekind domains and class groups of global fields . in L Cohen & C Kaliszyk (eds), 12th International Conference on Interactive Theorem Proving (ITP 2021) ., 5, Leibniz International Proceedings in Informatics, LIPIcs, vol. 193, Schloss Dagstuhl-Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 1-19, 12th International Conference on Interactive Theorem Proving, ITP 2021, Virtual, Rome, Italy, 29/06/21 . https://doi.org/10.4230/LIPIcs.ITP.2021.5
Baanen, A, Dahmen, S R, Narayanan, A & Nuccio Mortarino Majno di Capriglio, F A E 2022, ' A Formalization of Dedekind Domains and Class Groups of Global Fields ', Journal of Automated Reasoning, vol. 66, no. 4, pp. 611-637 . https://doi.org/10.1007/s10817-022-09644-0
12th International Conference on Interactive Theorem Proving (ITP 2021), 1-19
STARTPAGE=1;ENDPAGE=19;TITLE=12th International Conference on Interactive Theorem Proving (ITP 2021)
Journal of Automated Reasoning, 66(4), 611-637. Springer Netherlands

Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class group

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9bb17d640edab8c278236475e1f0392c

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.