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