Intelligent Computer Mathematics

.- Automated Reasoning .

.- Hammering Higher Order Set Theory.

.- Synthesis Benchmarks for Automated Reasoning.

.- Automated Symmetric Constructions in Discrete Geometry.

.- Formal Libraries .

.- Growing Mathlib: Maintenance of a Large Scale Mathematical Library.

.- Exploring Formal Math on the Blockchain: An Explorer for Proofgold.

.- Supporting Maintenance of Formal Mathematics with Similarity Search.

.- Logical and Linguistic Foundations .

.- Graded Quantitative Narrowing.

.- Equational Generalization Problems with Atom-Variables.

.- Extending Flexible Boolean Semantics for the Language of Mathematics.

.- A Formal Definition of an Algorithm Suitable for Parsing the Language of Mathematics.

.- Mathematical Knowledge Management .

.- Reaping the Benefits of Modularization in Flexiformal Mathematics by GFbased AST Transformations.

.- Semantic Authoring in a Flexiformal Context - Bulk Annotation of Rigorous Documents.

.- Michael Kohlhase and Jan Frederik Schaefer Lightweight Realms.

.- Indexing and Retrieval in a Heterogeneous Formal Library.

.- Neural Language Models .

.- Exploring Proof Autoformalization with Mistral on Herald.

.- Boosting Math Problem Solving in Small LLMs via Ensembles.

.- Proof Assistants and Formalizations .

.- Formalizing a Classification Theorem for Low-Dimensional Solvable Lie Algebras in Lean.

.- Certified Algorithms for Numerical Semigroups in Rocq.

.- Formalizing the Solow Model in Naproche.

.- Formalizing MLTL Formula Progression in Isabelle/HOL.

.- Formalising Fairness in the Assignment Problem with Ordinal Preferences in Isabelle/HOL.

.- A PVS Library on the Infinitude of Primes.

.- Vector Graphics through Category Theory.

.- A Lean-Based Language for Teaching Proof in High School.