Abstract is missing.
- Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math EquationsRuocheng Shan, Abdou Youssef. 3-20 [doi]
- Automated Mathematical Discovery and Verification: Minimizing Pentagons in the PlaneBernardo Subercaseaux, John Mackey, Marijn J. H. Heule, Ruben Martins. 21-41 [doi]
- Using General Large Language Models to Classify Mathematical DocumentsPatrick D. F. Ion, Stephen M. Watt. 42-57 [doi]
- Chaining Extensionality Lemmas in Lean's MathlibEric Wieser. 61-72 [doi]
- A Formalization of All Notions in the Statement of a Theorem by DeligneMichail Karatarakis. 73-90 [doi]
- Formalizing Finite Ramsey Theory in Lean 4David E. Narváez, Cruise Song, Ningxin Zhang. 91-108 [doi]
- Formalizing Pick's Theorem in Isabelle/HOLSage Binder, Katherine Kosaian. 109-126 [doi]
- Formalizing Coppersmith's Method in Isabelle/HOLKatherine Kosaian, Yong Kiam Tan, Kristin Yvonne Rozier. 127-145 [doi]
- Incorporating a Database of Graphs into a Proof AssistantAndrej Bauer, Katja Bercic, Gauvain Devillez, Jure Taslak. 146-162 [doi]
- Reusing Learning Objects via Theory MorphismsMichael Kohlhase, Marcel Schütz. 165-182 [doi]
- Transforming Optimization Problems into Disciplined Convex Programming FormRamon Fernández Mir, Paul B. Jackson, Siddharth Bhat, Andrés Goens, Tobias Grosser. 183-202 [doi]
- A Logical Framework Perspective on ConservativityFlorian Rabe 0001. 203-219 [doi]
- Towards Semantic Markup of Mathematical Documents via User InteractionLuka Vrecar, Joe B. Wells, Fairouz Kamareddine. 223-240 [doi]
- Evaluation and Domain Adaptation of Similarity Models for Short Mathematical TextsChristian Steinfeldt, Helena Mihaljevic. 241-260 [doi]
- Generating Formally Verified Quantum Fourier Transform AlgorithmsPatrick Brinich, Jeremy Johnson 0001. 261-276 [doi]
- Partial Proof Terms in the Study of Idealized Proof SearchJosé Espírito Santo, Ana Catarina Sousa. 279-297 [doi]
- A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem ProvingMohamed AbdelGhany, Adnan Rashid, Sofiène Tahar. 298-314 [doi]
- Solving Hard Mizar Problems with Instantiation and Strategy InventionJan Jakubuv, Mikolás Janota, Josef Urban. 315-333 [doi]
- Remote Verification System for Mizar Integrated with EmwikiToshiki Kai, Yuta Teruya, Kazuhisa Nakasho. 337-344 [doi]
- Oruga: Implementation and Use of Representational Systems TheoryDaniel Raggi, Gem Stapleton, Aaron Stockdill, Grecia Garcia Garcia, Peter C.-H. Cheng, Mateja Jamnik. 345-351 [doi]
- HOL4PRS: Proof Recommendation System for the HOL4 Theorem ProverNour Dekhil, Adnan Rashid, Sofiène Tahar. 352-359 [doi]