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