--- OA_place: repository OA_type: green _id: '17047' abstract: - lang: eng text: We provide a dynamical study of a model of multiplicative perturbation of a unitary matrix introduced by Fyodorov. In particular, we identify a flow of deterministic domains that bound the spectrum with high probability, separating the outlier from the typical eigenvalues at all sub-critical timescales. These results are obtained under generic assumptions on U that hold for a variety of unitary random matrix models. article_number: '2450007' article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 - first_name: Jana full_name: Reker, Jana id: e796e4f9-dc8d-11ea-abe3-97e26a0323e9 last_name: Reker citation: ama: 'Dubach G, Reker J. Dynamics of a rank-one multiplicative perturbation of a unitary matrix. Random Matrices: Theory and Applications. 2024;13(2). doi:10.1142/s2010326324500072' apa: 'Dubach, G., & Reker, J. (2024). Dynamics of a rank-one multiplicative perturbation of a unitary matrix. Random Matrices: Theory and Applications. World Scientific Publishing. https://doi.org/10.1142/s2010326324500072' chicago: 'Dubach, Guillaume, and Jana Reker. “Dynamics of a Rank-One Multiplicative Perturbation of a Unitary Matrix.” Random Matrices: Theory and Applications. World Scientific Publishing, 2024. https://doi.org/10.1142/s2010326324500072.' ieee: 'G. Dubach and J. Reker, “Dynamics of a rank-one multiplicative perturbation of a unitary matrix,” Random Matrices: Theory and Applications, vol. 13, no. 2. World Scientific Publishing, 2024.' ista: 'Dubach G, Reker J. 2024. Dynamics of a rank-one multiplicative perturbation of a unitary matrix. Random Matrices: Theory and Applications. 13(2), 2450007.' mla: 'Dubach, Guillaume, and Jana Reker. “Dynamics of a Rank-One Multiplicative Perturbation of a Unitary Matrix.” Random Matrices: Theory and Applications, vol. 13, no. 2, 2450007, World Scientific Publishing, 2024, doi:10.1142/s2010326324500072.' short: 'G. Dubach, J. Reker, Random Matrices: Theory and Applications 13 (2024).' corr_author: '1' date_created: 2024-05-23T08:31:57Z date_published: 2024-04-01T00:00:00Z date_updated: 2026-04-07T13:02:12Z day: '01' department: - _id: GradSch - _id: LaEr doi: 10.1142/s2010326324500072 ec_funded: 1 external_id: arxiv: - '2212.14638' isi: - '001229295200002' fulldoi: https://doi.org/10.1142/s2010326324500072 intvolume: ' 13' isi: 1 issue: '2' language: - iso: eng main_file_link: - open_access: '1' url: ' https://doi.org/10.48550/arXiv.2212.14638' month: '04' oa: 1 oa_version: Preprint project: - _id: 62796744-2b32-11ec-9570-940b20777f1d call_identifier: H2020 grant_number: '101020331' name: Random matrices beyond Wigner-Dyson-Mehta publication: 'Random Matrices: Theory and Applications' publication_identifier: eissn: - 2010-3271 issn: - 2010-3263 publication_status: published publisher: World Scientific Publishing quality_controlled: '1' related_material: record: - id: '17164' relation: dissertation_contains status: public scopus_import: '1' status: public title: Dynamics of a rank-one multiplicative perturbation of a unitary matrix type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 13 year: '2024' ... --- _id: '12683' abstract: - lang: eng text: We study the eigenvalue trajectories of a time dependent matrix Gt=H+itvv∗ for t≥0, where H is an N×N Hermitian random matrix and v is a unit vector. In particular, we establish that with high probability, an outlier can be distinguished at all times t>1+N−1/3+ϵ, for any ϵ>0. The study of this natural process combines elements of Hermitian and non-Hermitian analysis, and illustrates some aspects of the intrinsic instability of (even weakly) non-Hermitian matrices. acknowledgement: G. Dubach gratefully acknowledges funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411. L. Erdős is supported by ERC Advanced Grant “RMTBeyond” No. 101020331. article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 - first_name: László full_name: Erdös, László id: 4DBD5372-F248-11E8-B48F-1D18A9856A87 last_name: Erdös orcid: 0000-0001-5366-9603 citation: ama: Dubach G, Erdös L. Dynamics of a rank-one perturbation of a Hermitian matrix. Electronic Communications in Probability. 2023;28:1-13. doi:10.1214/23-ECP516 apa: Dubach, G., & Erdös, L. (2023). Dynamics of a rank-one perturbation of a Hermitian matrix. Electronic Communications in Probability. Institute of Mathematical Statistics. https://doi.org/10.1214/23-ECP516 chicago: Dubach, Guillaume, and László Erdös. “Dynamics of a Rank-One Perturbation of a Hermitian Matrix.” Electronic Communications in Probability. Institute of Mathematical Statistics, 2023. https://doi.org/10.1214/23-ECP516. ieee: G. Dubach and L. Erdös, “Dynamics of a rank-one perturbation of a Hermitian matrix,” Electronic Communications in Probability, vol. 28. Institute of Mathematical Statistics, pp. 1–13, 2023. ista: Dubach G, Erdös L. 2023. Dynamics of a rank-one perturbation of a Hermitian matrix. Electronic Communications in Probability. 28, 1–13. mla: Dubach, Guillaume, and László Erdös. “Dynamics of a Rank-One Perturbation of a Hermitian Matrix.” Electronic Communications in Probability, vol. 28, Institute of Mathematical Statistics, 2023, pp. 1–13, doi:10.1214/23-ECP516. short: G. Dubach, L. Erdös, Electronic Communications in Probability 28 (2023) 1–13. corr_author: '1' date_created: 2023-02-26T23:01:01Z date_published: 2023-02-08T00:00:00Z date_updated: 2025-04-14T07:44:00Z day: '08' ddc: - '510' department: - _id: LaEr doi: 10.1214/23-ECP516 ec_funded: 1 external_id: arxiv: - '2108.13694' isi: - '000950650200005' file: - access_level: open_access checksum: a1c6f0a3e33688fd71309c86a9aad86e content_type: application/pdf creator: dernst date_created: 2023-02-27T09:43:27Z date_updated: 2023-02-27T09:43:27Z file_id: '12692' file_name: 2023_ElectCommProbability_Dubach.pdf file_size: 479105 relation: main_file success: 1 file_date_updated: 2023-02-27T09:43:27Z fulldoi: https://doi.org/10.1214/23-ECP516 has_accepted_license: '1' intvolume: ' 28' isi: 1 language: - iso: eng month: '02' oa: 1 oa_version: Published Version page: 1-13 project: - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships - _id: 62796744-2b32-11ec-9570-940b20777f1d call_identifier: H2020 grant_number: '101020331' name: Random matrices beyond Wigner-Dyson-Mehta publication: Electronic Communications in Probability publication_identifier: eissn: - 1083-589X publication_status: published publisher: Institute of Mathematical Statistics quality_controlled: '1' scopus_import: '1' status: public title: Dynamics of a rank-one perturbation of a Hermitian matrix tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 28 year: '2023' ... --- _id: '17079' abstract: - lang: eng text: We study moments of characteristic polynomials of truncated Haar distributed matrices from the three classical compact groups O(N), U(N) and Sp(2N). For finite matrix size we calculate the moments in terms of hypergeometric functions of matrix argument and give explicit integral representations highlighting the duality between the moment and the matrix size as well as the duality between the orthogonal and symplectic cases. Asymptotic expansions in strong and weak non-unitarity regimes are obtained. Using the connection to matrix hypergeometric functions, we establish limit theorems for the log-modulus of the characteristic polynomial evaluated on the unit circle. acknowledgement: N.S. gratefully acknowledges financial support of the Royal Society, grant URF/R1/180707. We would like to thank Emma Bailey, Yan Fyodorov and Jordan Stoyanov for helpful comments an an earlier version of this paper. We are grateful for the comments of an anonymous referee. article_number: '2250049' article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Alexander full_name: Serebryakov, Alexander last_name: Serebryakov - first_name: Nick full_name: Simm, Nick last_name: Simm - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 citation: ama: 'Serebryakov A, Simm N, Dubach G. Characteristic polynomials of random truncations: Moments, duality and asymptotics. Random Matrices: Theory and Applications. 2023;12(01). doi:10.1142/s2010326322500496' apa: 'Serebryakov, A., Simm, N., & Dubach, G. (2023). Characteristic polynomials of random truncations: Moments, duality and asymptotics. Random Matrices: Theory and Applications. World Scientific Publishing. https://doi.org/10.1142/s2010326322500496' chicago: 'Serebryakov, Alexander, Nick Simm, and Guillaume Dubach. “Characteristic Polynomials of Random Truncations: Moments, Duality and Asymptotics.” Random Matrices: Theory and Applications. World Scientific Publishing, 2023. https://doi.org/10.1142/s2010326322500496.' ieee: 'A. Serebryakov, N. Simm, and G. Dubach, “Characteristic polynomials of random truncations: Moments, duality and asymptotics,” Random Matrices: Theory and Applications, vol. 12, no. 01. World Scientific Publishing, 2023.' ista: 'Serebryakov A, Simm N, Dubach G. 2023. Characteristic polynomials of random truncations: Moments, duality and asymptotics. Random Matrices: Theory and Applications. 12(01), 2250049.' mla: 'Serebryakov, Alexander, et al. “Characteristic Polynomials of Random Truncations: Moments, Duality and Asymptotics.” Random Matrices: Theory and Applications, vol. 12, no. 01, 2250049, World Scientific Publishing, 2023, doi:10.1142/s2010326322500496.' short: 'A. Serebryakov, N. Simm, G. Dubach, Random Matrices: Theory and Applications 12 (2023).' date_created: 2024-05-29T06:14:26Z date_published: 2023-01-01T00:00:00Z date_updated: 2025-09-09T14:27:10Z day: '01' department: - _id: LaEr doi: 10.1142/s2010326322500496 external_id: arxiv: - '2109.10331' isi: - '000848874400001' fulldoi: https://doi.org/10.1142/s2010326322500496 intvolume: ' 12' isi: 1 issue: '01' language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.2109.10331 month: '01' oa: 1 oa_version: Preprint publication: 'Random Matrices: Theory and Applications' publication_identifier: eissn: - 2010-3271 issn: - 2010-3263 publication_status: published publisher: World Scientific Publishing quality_controlled: '1' scopus_import: '1' status: public title: 'Characteristic polynomials of random truncations: Moments, duality and asymptotics' type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 12 year: '2023' ... --- _id: '15259' abstract: - lang: eng text: "We consider words Gi1⋯Gim involving i.i.d. complex Ginibre matrices and study tracial expressions of their eigenvalues and singular values. We show that the limit distribution of the squared singular values of every word of length m is a Fuss–Catalan distribution with parameter \r\nm+1. This generalizes previous results concerning powers of a complex Ginibre matrix and products of independent Ginibre matrices. In addition, we find other combinatorial parameters of the word that determine the second-order limits of the spectral statistics. For instance, the so-called coperiod of a word characterizes the fluctuations of the eigenvalues. We extend these results to words of general non-Hermitian matrices with i.i.d. entries under moment-matching assumptions, band matrices, and sparse matrices.\r\nThese results rely on the moments method and genus expansion, relating Gaussian matrix integrals to the counting of compact orientable surfaces of a given genus. This allows us to derive a central limit theorem for the trace of any word of complex Ginibre matrices and their conjugate transposes, where all parameters are defined topologically." acknowledgement: "The authors would like to thank Gernot Akemann, Benson Au, Paul Bourgade, Jesper Ipsen, Camille Male, Jamie Mingo, Doron Puder, Emily Redelmeier, Roland Speicher, Wojciech Tarnowski and Ofer Zeitouni for useful discussions, comments and references as well as the anonymous referee for a suggestion that greatly improved one of the theorems.\r\nG.D. gratefully acknowledges support from the grants NSF DMS-1812114 of P. Bourgade (PI) and NSF CAREER DMS-1653602 of L.-P. Arguin (PI), as well as the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411." article_processing_charge: No article_type: original arxiv: 1 author: - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 - first_name: Yuval full_name: Peled, Yuval last_name: Peled citation: ama: Dubach G, Peled Y. On words of non-Hermitian random matrices. The Annals of Probability. 2021;49(4):1886-1916. doi:10.1214/20-aop1496 apa: Dubach, G., & Peled, Y. (2021). On words of non-Hermitian random matrices. The Annals of Probability. Institute of Mathematical Statistics. https://doi.org/10.1214/20-aop1496 chicago: Dubach, Guillaume, and Yuval Peled. “On Words of Non-Hermitian Random Matrices.” The Annals of Probability. Institute of Mathematical Statistics, 2021. https://doi.org/10.1214/20-aop1496. ieee: G. Dubach and Y. Peled, “On words of non-Hermitian random matrices,” The Annals of Probability, vol. 49, no. 4. Institute of Mathematical Statistics, pp. 1886–1916, 2021. ista: Dubach G, Peled Y. 2021. On words of non-Hermitian random matrices. The Annals of Probability. 49(4), 1886–1916. mla: Dubach, Guillaume, and Yuval Peled. “On Words of Non-Hermitian Random Matrices.” The Annals of Probability, vol. 49, no. 4, Institute of Mathematical Statistics, 2021, pp. 1886–916, doi:10.1214/20-aop1496. short: G. Dubach, Y. Peled, The Annals of Probability 49 (2021) 1886–1916. corr_author: '1' date_created: 2024-04-03T07:19:42Z date_published: 2021-07-01T00:00:00Z date_updated: 2025-09-10T10:13:20Z day: '01' department: - _id: LaEr doi: 10.1214/20-aop1496 ec_funded: 1 external_id: arxiv: - '1904.04312' isi: - '000681349000008' fulldoi: https://doi.org/10.1214/20-aop1496 intvolume: ' 49' isi: 1 issue: '4' keyword: - Statistics - Probability and Uncertainty - Statistics and Probability language: - iso: eng main_file_link: - open_access: '1' url: https://doi.org/10.48550/arXiv.1904.04312 month: '07' oa: 1 oa_version: Preprint page: 1886-1916 project: - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships publication: The Annals of Probability publication_identifier: issn: - 0091-1798 publication_status: published publisher: Institute of Mathematical Statistics quality_controlled: '1' scopus_import: '1' status: public title: On words of non-Hermitian random matrices type: journal_article user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345 volume: 49 year: '2021' ... --- _id: '10285' abstract: - lang: eng text: We study the overlaps between right and left eigenvectors for random matrices of the spherical ensemble, as well as truncated unitary ensembles in the regime where half of the matrix at least is truncated. These two integrable models exhibit a form of duality, and the essential steps of our investigation can therefore be performed in parallel. In every case, conditionally on all eigenvalues, diagonal overlaps are shown to be distributed as a product of independent random variables with explicit distributions. This enables us to prove that the scaled diagonal overlaps, conditionally on one eigenvalue, converge in distribution to a heavy-tail limit, namely, the inverse of a γ2 distribution. We also provide formulae for the conditional expectation of diagonal and off-diagonal overlaps, either with respect to one eigenvalue, or with respect to the whole spectrum. These results, analogous to what is known for the complex Ginibre ensemble, can be obtained in these cases thanks to integration techniques inspired from a previous work by Forrester & Krishnapur. acknowledgement: We acknowledge partial support from the grants NSF DMS-1812114 of P. Bourgade (PI) and NSF CAREER DMS-1653602 of L.-P. Arguin (PI). This project has also received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411. We would like to thank Paul Bourgade and László Erdős for many helpful comments. article_number: '124' article_processing_charge: No article_type: original author: - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 citation: ama: Dubach G. On eigenvector statistics in the spherical and truncated unitary ensembles. Electronic Journal of Probability. 2021;26. doi:10.1214/21-EJP686 apa: Dubach, G. (2021). On eigenvector statistics in the spherical and truncated unitary ensembles. Electronic Journal of Probability. Institute of Mathematical Statistics. https://doi.org/10.1214/21-EJP686 chicago: Dubach, Guillaume. “On Eigenvector Statistics in the Spherical and Truncated Unitary Ensembles.” Electronic Journal of Probability. Institute of Mathematical Statistics, 2021. https://doi.org/10.1214/21-EJP686. ieee: G. Dubach, “On eigenvector statistics in the spherical and truncated unitary ensembles,” Electronic Journal of Probability, vol. 26. Institute of Mathematical Statistics, 2021. ista: Dubach G. 2021. On eigenvector statistics in the spherical and truncated unitary ensembles. Electronic Journal of Probability. 26, 124. mla: Dubach, Guillaume. “On Eigenvector Statistics in the Spherical and Truncated Unitary Ensembles.” Electronic Journal of Probability, vol. 26, 124, Institute of Mathematical Statistics, 2021, doi:10.1214/21-EJP686. short: G. Dubach, Electronic Journal of Probability 26 (2021). date_created: 2021-11-14T23:01:25Z date_published: 2021-09-28T00:00:00Z date_updated: 2025-04-14T07:43:47Z day: '28' ddc: - '519' department: - _id: LaEr doi: 10.1214/21-EJP686 ec_funded: 1 file: - access_level: open_access checksum: 1c975afb31460277ce4d22b93538e5f9 content_type: application/pdf creator: cchlebak date_created: 2021-11-15T10:10:17Z date_updated: 2021-11-15T10:10:17Z file_id: '10288' file_name: 2021_ElecJournalProb_Dubach.pdf file_size: 735940 relation: main_file success: 1 file_date_updated: 2021-11-15T10:10:17Z fulldoi: https://doi.org/10.1214/21-EJP686 has_accepted_license: '1' intvolume: ' 26' language: - iso: eng month: '09' oa: 1 oa_version: Published Version project: - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships publication: Electronic Journal of Probability publication_identifier: eissn: - 1083-6489 publication_status: published publisher: Institute of Mathematical Statistics quality_controlled: '1' scopus_import: '1' status: public title: On eigenvector statistics in the spherical and truncated unitary ensembles tmp: image: /images/cc_by.png legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0) short: CC BY (4.0) type: journal_article user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9 volume: 26 year: '2021' ... --- _id: '9230' abstract: - lang: eng text: "We consider a model of the Riemann zeta function on the critical axis and study its maximum over intervals of length (log T)θ, where θ is either fixed or tends to zero at a suitable rate.\r\nIt is shown that the deterministic level of the maximum interpolates smoothly between the ones\r\nof log-correlated variables and of i.i.d. random variables, exhibiting a smooth transition ‘from\r\n3/4 to 1/4’ in the second order. This provides a natural context where extreme value statistics of\r\nlog-correlated variables with time-dependent variance and rate occur. A key ingredient of the\r\nproof is a precise upper tail tightness estimate for the maximum of the model on intervals of\r\nsize one, that includes a Gaussian correction. This correction is expected to be present for the\r\nRiemann zeta function and pertains to the question of the correct order of the maximum of\r\nthe zeta function in large intervals." acknowledgement: The research of L.-P. A. is supported in part by the grant NSF CAREER DMS-1653602. G. D. gratefully acknowledges support from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 754411. The research of L. H. is supported in part by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) through Project-ID 233630050 -TRR 146, Project-ID 443891315 within SPP 2265 and Project-ID 446173099. article_number: '2103.04817' article_processing_charge: No arxiv: 1 author: - first_name: Louis-Pierre full_name: Arguin, Louis-Pierre last_name: Arguin - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 - first_name: Lisa full_name: Hartung, Lisa last_name: Hartung citation: ama: Arguin L-P, Dubach G, Hartung L. Maxima of a random model of the Riemann zeta function over intervals of varying length. arXiv. doi:10.48550/arXiv.2103.04817 apa: Arguin, L.-P., Dubach, G., & Hartung, L. (n.d.). Maxima of a random model of the Riemann zeta function over intervals of varying length. arXiv. https://doi.org/10.48550/arXiv.2103.04817 chicago: Arguin, Louis-Pierre, Guillaume Dubach, and Lisa Hartung. “Maxima of a Random Model of the Riemann Zeta Function over Intervals of Varying Length.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2103.04817. ieee: L.-P. Arguin, G. Dubach, and L. Hartung, “Maxima of a random model of the Riemann zeta function over intervals of varying length,” arXiv. . ista: Arguin L-P, Dubach G, Hartung L. Maxima of a random model of the Riemann zeta function over intervals of varying length. arXiv, 2103.04817. mla: Arguin, Louis-Pierre, et al. “Maxima of a Random Model of the Riemann Zeta Function over Intervals of Varying Length.” ArXiv, 2103.04817, doi:10.48550/arXiv.2103.04817. short: L.-P. Arguin, G. Dubach, L. Hartung, ArXiv (n.d.). date_created: 2021-03-09T11:08:15Z date_published: 2021-03-08T00:00:00Z date_updated: 2025-04-14T07:43:51Z day: '08' department: - _id: LaEr doi: 10.48550/arXiv.2103.04817 ec_funded: 1 external_id: arxiv: - '2103.04817' fulldoi: https://doi.org/10.48550/arXiv.2103.04817 language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/2103.04817 month: '03' oa: 1 oa_version: Preprint project: - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships publication: arXiv publication_status: submitted status: public title: Maxima of a random model of the Riemann zeta function over intervals of varying length type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2021' ... --- _id: '9281' abstract: - lang: eng text: We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's recent new proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics. article_number: '2103.11389' article_processing_charge: No arxiv: 1 author: - first_name: Guillaume full_name: Dubach, Guillaume id: D5C6A458-10C4-11EA-ABF4-A4B43DDC885E last_name: Dubach orcid: 0000-0001-6892-8137 - first_name: Fabian full_name: Mühlböck, Fabian id: 6395C5F6-89DF-11E9-9C97-6BDFE5697425 last_name: Mühlböck orcid: 0000-0003-1548-0177 citation: ama: Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv. doi:10.48550/arXiv.2103.11389 apa: Dubach, G., & Mühlböck, F. (n.d.). Formal verification of Zagier’s one-sentence proof. arXiv. https://doi.org/10.48550/arXiv.2103.11389 chicago: Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2103.11389. ieee: G. Dubach and F. Mühlböck, “Formal verification of Zagier’s one-sentence proof,” arXiv. . ista: Dubach G, Mühlböck F. Formal verification of Zagier’s one-sentence proof. arXiv, 2103.11389. mla: Dubach, Guillaume, and Fabian Mühlböck. “Formal Verification of Zagier’s One-Sentence Proof.” ArXiv, 2103.11389, doi:10.48550/arXiv.2103.11389. short: G. Dubach, F. Mühlböck, ArXiv (n.d.). corr_author: '1' date_created: 2021-03-23T05:38:48Z date_published: 2021-03-21T00:00:00Z date_updated: 2025-04-15T06:26:12Z day: '21' department: - _id: LaEr - _id: ToHe doi: 10.48550/arXiv.2103.11389 ec_funded: 1 external_id: arxiv: - '2103.11389' fulldoi: https://doi.org/10.48550/arXiv.2103.11389 language: - iso: eng main_file_link: - open_access: '1' url: https://arxiv.org/abs/2103.11389 month: '03' oa: 1 oa_version: Preprint project: - _id: 260C2330-B435-11E9-9278-68D0E5697425 call_identifier: H2020 grant_number: '754411' name: ISTplus - Postdoctoral Fellowships publication: arXiv publication_status: submitted related_material: record: - id: '9946' relation: other status: public status: public title: Formal verification of Zagier's one-sentence proof type: preprint user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 year: '2021' ...