.- AI and LLM.
.- Using Large Language Models to Automate Annotation and Part-of-Math Tagging of Math Equations.
.- Automated Mathematical Discovery and Veri?cation: Minimizing Pentagons in the Plane.
.- Using General Large Language Models to Classify Mathematical Documents.
.- Proof Assistants.
.- Chaining extensionality lemmas in Lean’s Mathlib.
.- A formalization of all notions in the statement of a theorem by Deligne.
.- Formalizing Finite Ramsey Theory in Lean 4.
.- Formalizing Pick’s Theorem in Isabelle/HOL.
.- Formalizing Coppersmith’s Method in Isabelle/HOL.
.- Incorporating a database of graphs into a proof assistant.
.- Logical Frameworks and Transformations.
.- Reusing Learning Objects via Theory Morphisms.
.- Transforming Optimization Problems into Disciplined Convex Programming Form.
.- A Logical Framework Perspective on Conservativity.
.- Knowledge Representation and Certi?cation.
.- Towards Semantic Markup of Mathematical Documents via User Interaction.
.- Evaluation and Domain Adaptation of Similarity Models for Short Mathematical Texts.
.- Generating Formally Veri?ed Quantum Fourier Transform Algorithms.
.- Proof Search and Formalization.
.- Partial proof terms in the study of idealized proof search.
.- A Framework for Formal Probabilistic Risk Assessment using HOL Theorem Proving.
.- Solving Hard Mizar Problems with Instantiation and Strategy Invention.
.- System Descriptions.
.- Remote Veri?cation System for Mizar Integrated with Emwiki.
.- Oruga: Implementation and Use of Representational Systems Theory.
.- HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover.
