Want to learn more about the latest developments on using AI and (interactive) theorem proving in Mathematics? Wait no longer!
We have a great line-up of speakers at our online Workshop on AI and Theorem Provers in Mathematics. The workshop will be held online from 8th to 10th of April and attendance is free (registration required). For more details, visit the workshop website: https://aitpm.github.io/
#math #itp #theoremProving #isabelleHOL #lean #llm #ai #formal_mehods #agda #hol #mathematics
We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate the relationships between them and their classical counterparts. We identify, and eliminate where possible, the use of classical logic in the proofs of standard ARS results. Our analysis leads to refinements and mild generalizations of classical termination and confluence criteria. We investigate logical relationships between several notions of termination, arising from different formulations of the concept of a well-founded relation. We illustrate general applicability of our ARS development with an example formalization of the lambda calculus.
The schedule for the 2026 PhD course "Functional Programming and Climate Impact Research" (FPClimate) is now live!
We kick off on March 23, reading and discussing papers on the application of FP, DSLs, and dependent types to climate modeling, decision problems, and policy advice.
Remote participation is available! External participants are very welcome to join the seminars and discussions (though we cannot issue formal university credits for externals).
Details & reading list: https://github.com/DSLsofMath/FPClimate
Blog post: https://patrikja.owlstown.net/posts/5275
#FunctionalProgramming #ClimateScience #Haskell #Agda #FormalMethods #AcademicMastodon
Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the situation by integrating proof assistants with automated theorem provers (ATPs) in a simple way, while preserving the correctness guarantees of the former. A central difficulty arises from the fact that most ATPs operate in classical first-order logic, whereas these proof assistants are grounded in constructive dependent type theory. We identify an expressive fragment of both languages -- essentially equational Horn -- that admits sound, straightforward translations in both directions. The approach produces a prototype system for Agda forwarding proof obligations to the ATP Vampire, then transforming the resulting classical proof into a constructive proof term that Agda can type-check. The prototype automatically derives proofs concerning the properties of a complex field equipped with roots of unity, which took professional Agda developers two full days to complete. The required engineering effort is modest, and we anticipate that the methodology will extend readily to other ATPs and proof assistants.
The objective of automata learning is to reconstruct the implementation of a hidden automaton, to which only a teacher has access. The learner can ask certain kinds of queries to the teacher to gain more knowledge about the hidden automaton. The run-time of such a learning algorithm is then measured in the number of queries it takes until the hidden automaton is successfully reconstructed, which is usually parametric in the number of states of that hidden automaton. How can we prove such a run-time complexity of learning algorithms in a proof assistant if we do not have the hidden automaton and the number of states available? In the present paper, we solve this by considering learning algorithms themselves as generalized automata, more specifically as coalgebras. We introduce formal and yet compact definitions of what a learner and a teacher is, which make it easy to prove upper and lower bounds of different kinds of learning games in the proof assistant Agda. As a running example, we discuss the common number guessing game where a teacher thinks of a natural number and answers guesses by the learner with `correct', `too high', or `too low'. To demonstrate our framework, we formally prove in Agda that both the lower and upper bound on number of guesses by the learner is $\mathcal{O}(\log n)$, where $n$ is the teacher's secret number.
Achim D. Brucker
Fraser Tweedale
José A. Alonso
HoldMyType
Linotype Pilgrim
Patrik Jansson
