Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro; Steinberg, Matías The formal verification of the ctm approach to forcing. (English) Zbl 07815139 Ann. Pure Appl. Logic 175, No. 5, Article ID 103413, 28 p. (2024). MSC: 68V20 03E35 03E30 03E04 PDFBibTeX XMLCite \textit{E. Gunther} et al., Ann. Pure Appl. Logic 175, No. 5, Article ID 103413, 28 p. (2024; Zbl 07815139) Full Text: DOI arXiv
Paulson, Lawrence C. A formalised theorem in the partition calculus. (English) Zbl 07748742 Ann. Pure Appl. Logic 175, No. 1, Article ID 103246, 10 p. (2024). MSC: 03E02 03E10 03B35 68V15 68V20 PDFBibTeX XMLCite \textit{L. C. Paulson}, Ann. Pure Appl. Logic 175, No. 1, Article ID 103246, 10 p. (2024; Zbl 07748742) Full Text: DOI arXiv
Buzzard, Kevin What is the point of computers? A question for pure mathematicians. (English) Zbl 07821721 Beliaev, Dmitry (ed.) et al., International congress of mathematicians 2022, ICM 2022, Helsinki, Finland, virtual, July 6–14, 2022. Volume 2. Plenary lectures. Berlin: European Mathematical Society (EMS). 578-608 (2023). MSC: 68V20 PDFBibTeX XMLCite \textit{K. Buzzard}, in: International congress of mathematicians 2022, ICM 2022, Helsinki, Finland, virtual, July 6--14, 2022. Volume 2. Plenary lectures. Berlin: European Mathematical Society (EMS). 578--608 (2023; Zbl 07821721) Full Text: DOI arXiv OA License
Schaefer, Jan Frederik; Kohlhase, Michael Towards an annotation standard for STEM documents. Datasets, benchmarks, and spotters. (English) Zbl 07810732 Dubois, Catherine (ed.) et al., Intelligent computer mathematics. 16th international conference, CICM 2023, Cambridge, UK, September 5–8, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14101, 190-205 (2023). MSC: 68Vxx PDFBibTeX XMLCite \textit{J. F. Schaefer} and \textit{M. Kohlhase}, Lect. Notes Comput. Sci. 14101, 190--205 (2023; Zbl 07810732) Full Text: DOI
Paulson, Lawrence C. Large-scale formal proof for the working mathematician – lessons learnt from the ALEXANDRIA project. (English) Zbl 07810720 Dubois, Catherine (ed.) et al., Intelligent computer mathematics. 16th international conference, CICM 2023, Cambridge, UK, September 5–8, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14101, 3-15 (2023). MSC: 68Vxx PDFBibTeX XMLCite \textit{L. C. Paulson}, Lect. Notes Comput. Sci. 14101, 3--15 (2023; Zbl 07810720) Full Text: DOI arXiv
Colbrook, Matthew J.; Hansen, Anders C. The foundations of spectral computations via the solvability complexity index hierarchy. (English) Zbl 07774915 J. Eur. Math. Soc. (JEMS) 25, No. 12, 4639-4718 (2023). MSC: 68Q15 47A10 46N40 35P15 65L15 65N25 PDFBibTeX XMLCite \textit{M. J. Colbrook} and \textit{A. C. Hansen}, J. Eur. Math. Soc. (JEMS) 25, No. 12, 4639--4718 (2023; Zbl 07774915) Full Text: DOI arXiv
Koprowski, Przemysław; Magron, Victor; Vaccon, Tristan Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares. (English) Zbl 07760788 Dickenstein, Alicia (ed.) et al., Proceedings of the 48th international symposium on symbolic and algebraic computation, ISSAC, Tromsø, Norway, July 24–27, 2023. New York, NY: Association for Computing Machinery (ACM). 425-433 (2023). MSC: 68W30 PDFBibTeX XMLCite \textit{P. Koprowski} et al., in: Proceedings of the 48th international symposium on symbolic and algebraic computation, ISSAC, Tromsø, Norway, July 24--27, 2023. New York, NY: Association for Computing Machinery (ACM). 425--433 (2023; Zbl 07760788) Full Text: DOI arXiv
Fernique, Thomas; Pchelina, Daria Density of triangulated ternary disc packings. (English) Zbl 1519.52014 Comput. Geom. 115, Article ID 102032, 26 p. (2023). MSC: 52C15 68U05 PDFBibTeX XMLCite \textit{T. Fernique} and \textit{D. Pchelina}, Comput. Geom. 115, Article ID 102032, 26 p. (2023; Zbl 1519.52014) Full Text: DOI arXiv
Mangla, Chaitanya; Holden, Sean B.; Paulson, Lawrence C. Bayesian ranking for strategy scheduling in automated theorem provers. (English) Zbl 1520.68216 Blanchette, Jasmin (ed.) et al., Automated reasoning. 11th international joint conference, IJCAR 2022, Haifa, Israel, August 8–10, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13385, 559-577 (2022). Reviewer: Truong Hoang Le (Hà Nội) MSC: 68V15 68T05 68T20 PDFBibTeX XMLCite \textit{C. Mangla} et al., Lect. Notes Comput. Sci. 13385, 559--577 (2022; Zbl 1520.68216) Full Text: DOI
Miyazawa, Flávio K.; Wakabayashi, Yoshiko Techniques and results on approximation algorithms for packing circles. (English) Zbl 1520.68222 São Paulo J. Math. Sci. 16, No. 1, 585-615 (2022). Reviewer: Truong Hoang Le (Hà Nội) MSC: 68W25 52C17 52C26 68Q17 68W27 90C27 PDFBibTeX XMLCite \textit{F. K. Miyazawa} and \textit{Y. Wakabayashi}, São Paulo J. Math. Sci. 16, No. 1, 585--615 (2022; Zbl 1520.68222) Full Text: DOI
Koutsoukou-Argyraki, Angeliki; Li, Wenda; Paulson, Lawrence C. Irrationality and transcendence criteria for infinite series in Isabelle/HOL. (English) Zbl 1518.11003 Exp. Math. 31, No. 2, 401-412 (2022). Reviewer: Alexandra Shlapentokh (Greenville) MSC: 11-04 11J81 11J68 68V20 03B35 68V35 PDFBibTeX XMLCite \textit{A. Koutsoukou-Argyraki} et al., Exp. Math. 31, No. 2, 401--412 (2022; Zbl 1518.11003) Full Text: DOI arXiv
Džamonja, Mirna; Koutsoukou-Argyraki, Angeliki; Paulson, Lawrence C. Formalizing ordinal partition relations using Isabelle/HOL. (English) Zbl 1520.68217 Exp. Math. 31, No. 2, 383-400 (2022). Reviewer: Truong Hoang Le (Hà Nội) MSC: 68V20 03B35 03E02 03E05 PDFBibTeX XMLCite \textit{M. Džamonja} et al., Exp. Math. 31, No. 2, 383--400 (2022; Zbl 1520.68217) Full Text: DOI arXiv
Dubut, Jérémy; Yamada, Akihisa Fixed points theorems for non-transitive relations. (English) Zbl 07471719 Log. Methods Comput. Sci. 18, No. 1, Paper No. 30, 24 p. (2022). MSC: 03B70 68-XX PDFBibTeX XMLCite \textit{J. Dubut} and \textit{A. Yamada}, Log. Methods Comput. Sci. 18, No. 1, Paper No. 30, 24 p. (2022; Zbl 07471719) Full Text: arXiv Link
Avigad, Jeremy Varieties of mathematical understanding. (English) Zbl 1482.00005 Bull. Am. Math. Soc., New Ser. 59, No. 1, 99-117 (2022). Reviewer: Truong Hoang Le (Hanoi) MSC: 00A30 01A67 52-02 52-08 68Vxx PDFBibTeX XMLCite \textit{J. Avigad}, Bull. Am. Math. Soc., New Ser. 59, No. 1, 99--117 (2022; Zbl 1482.00005) Full Text: DOI
Rabe, Markus N.; Szegedy, Christian Towards the automatic mathematician. (English) Zbl 1510.68116 Platzer, André (ed.) et al., Automated deduction – CADE 28. 28th international conference on automated deduction, virtual event, July 12–15, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12699, 25-37 (2021). Reviewer: Truong Hoang Le (Hà Nội) MSC: 68V15 68T05 68T50 68V20 PDFBibTeX XMLCite \textit{M. N. Rabe} and \textit{C. Szegedy}, Lect. Notes Comput. Sci. 12699, 25--37 (2021; Zbl 1510.68116) Full Text: DOI
Fervari, Raul; Trucco, Francisco; Ziliani, Beta Verification of dynamic bisimulation theorems in Coq. (English) Zbl 1518.68418 J. Log. Algebr. Methods Program. 120, Article ID 100642, 19 p. (2021). MSC: 68V20 03B45 03B70 PDFBibTeX XMLCite \textit{R. Fervari} et al., J. Log. Algebr. Methods Program. 120, Article ID 100642, 19 p. (2021; Zbl 1518.68418) Full Text: DOI
Färber, Michael; Kaliszyk, Cezary; Urban, Josef Machine learning guidance for connection tableaux. (English) Zbl 07356974 J. Autom. Reasoning 65, No. 2, 287-320 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{M. Färber} et al., J. Autom. Reasoning 65, No. 2, 287--320 (2021; Zbl 07356974) Full Text: DOI
Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge. (English) Zbl 1493.68391 Math. Intell. 43, No. 1, 78-87 (2021). Reviewer: Truong Hoang Le (Hanoi) MSC: 68Vxx 00A30 00A35 01A65 01A67 PDFBibTeX XMLCite \textit{J. Carette} et al., Math. Intell. 43, No. 1, 78--87 (2021; Zbl 1493.68391) Full Text: DOI
Koutsoukou-Argyraki, Angeliki Formalising mathematics – in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started. (English) Zbl 1495.68241 Jahresber. Dtsch. Math.-Ver. 123, No. 1, 3-26 (2021). Reviewer: Truong Hoang Le (Hanoi) MSC: 68V20 03B35 68V15 68V35 PDFBibTeX XMLCite \textit{A. Koutsoukou-Argyraki}, Jahresber. Dtsch. Math.-Ver. 123, No. 1, 3--26 (2021; Zbl 1495.68241) Full Text: DOI Backlinks: MO
Yamada, Akihisa; Dubut, Jérémy Complete non-orders and fixed points. (English) Zbl 07649979 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 30, 16 p. (2019). MSC: 68V20 PDFBibTeX XMLCite \textit{A. Yamada} and \textit{J. Dubut}, LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 30, 16 p. (2019; Zbl 07649979) Full Text: DOI
Dahmen, Sander R.; Hölzl, Johannes; Lewis, Robert Y. Formalizing the solution to the cap set problem. (English) Zbl 07649964 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 15, 19 p. (2019). MSC: 68V20 PDFBibTeX XMLCite \textit{S. R. Dahmen} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 15, 19 p. (2019; Zbl 07649964) Full Text: DOI arXiv
Brown, Chad E.; Kaliszyk, Cezary; Pak, Karol Higher-order Tarski Grothendieck as a foundation for formal proof. (English) Zbl 07649958 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 9, 16 p. (2019). MSC: 68V20 PDFBibTeX XMLCite \textit{C. E. Brown} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 9, 16 p. (2019; Zbl 07649958) Full Text: DOI
Bertholon, Guillaume; Martin-Dorel, Érik; Roux, Pierre Primitive floats in Coq. (English) Zbl 07649956 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 7, 20 p. (2019). MSC: 68V15 PDFBibTeX XMLCite \textit{G. Bertholon} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 7, 20 p. (2019; Zbl 07649956) Full Text: DOI
Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius From LCF to Isabelle/HOL. (English) Zbl 1427.68349 Formal Asp. Comput. 31, No. 6, 675-698 (2019). MSC: 68V15 68-03 PDFBibTeX XMLCite \textit{L. C. Paulson} et al., Formal Asp. Comput. 31, No. 6, 675--698 (2019; Zbl 1427.68349) Full Text: DOI arXiv
Gunther, Emmanuel; Pagano, Miguel; Sánchez Terraf, Pedro First steps towards a formalization of forcing. (English) Zbl 1434.03029 Accattoli, Beniamino (ed.) et al., Proceedings of the 13th workshop on logical and semantic frameworks with applications, LSFA 18, Fortaleza, Brazil, September 26–28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 344, 119-136 (2019). MSC: 03B35 03E35 68V20 PDFBibTeX XMLCite \textit{E. Gunther} et al., Electron. Notes Theor. Comput. Sci. 344, 119--136 (2019; Zbl 1434.03029) Full Text: DOI arXiv
Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong Formalization of geometric algebra in HOL Light. (English) Zbl 1468.68329 J. Autom. Reasoning 63, No. 3, 787-808 (2019). MSC: 68V20 15A66 PDFBibTeX XMLCite \textit{L.-M. Li} et al., J. Autom. Reasoning 63, No. 3, 787--808 (2019; Zbl 1468.68329) Full Text: DOI
Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol The role of the Mizar mathematical library for interactive proof development in Mizar. (English) Zbl 1433.68530 J. Autom. Reasoning 61, No. 1-4, 9-32 (2018). MSC: 68V15 68V20 68V30 PDFBibTeX XMLCite \textit{G. Bancerek} et al., J. Autom. Reasoning 61, No. 1--4, 9--32 (2018; Zbl 1433.68530) Full Text: DOI
Alt, Helmut; Buchin, Kevin; Chaplick, Steven; Cheong, Otfried; Kindermann, Philipp; Knauer, Christian; Stehn, Fabian Placing your coins on a shelf. (English) Zbl 1457.68273 Okamoto, Yoshio (ed.) et al., 28th international symposium on algorithms and computation, ISAAC 2017, December 9–12, 2017, Phuket, Thailand. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 92, Article 4, 12 p. (2017). MSC: 68U05 68Q17 68W25 PDFBibTeX XMLCite \textit{H. Alt} et al., LIPIcs -- Leibniz Int. Proc. Inform. 92, Article 4, 12 p. (2017; Zbl 1457.68273) Full Text: DOI arXiv
Ganesalingam, M.; Gowers, W. T. A fully automatic theorem prover with human-style output. (English) Zbl 1405.03035 J. Autom. Reasoning 58, No. 2, 253-291 (2017). MSC: 03B35 68T15 PDFBibTeX XMLCite \textit{M. Ganesalingam} and \textit{W. T. Gowers}, J. Autom. Reasoning 58, No. 2, 253--291 (2017; Zbl 1405.03035) Full Text: DOI
Aransay, Jesús; Divasón, Jose A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem. (English) Zbl 1409.68249 J. Autom. Reasoning 58, No. 4, 509-535 (2017). MSC: 68T15 03B35 15A24 PDFBibTeX XMLCite \textit{J. Aransay} and \textit{J. Divasón}, J. Autom. Reasoning 58, No. 4, 509--535 (2017; Zbl 1409.68249) Full Text: DOI
Köppe, Matthias; Zhou, Yuan Toward computer-assisted discovery and automated proofs of cutting plane theorems. (English) Zbl 1445.68329 Cerulli, Raffaele (ed.) et al., Combinatorial optimization. 4th international symposium, ISCO 2016, Vietri sul Mare, Italy, May 16–18, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 9849, 332-344 (2016). MSC: 68V15 90C10 90C11 PDFBibTeX XMLCite \textit{M. Köppe} and \textit{Y. Zhou}, Lect. Notes Comput. Sci. 9849, 332--344 (2016; Zbl 1445.68329) Full Text: DOI arXiv