Intelligent Computer Mathematics

.- 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.