Related papers: The Equational Theories Project: Advancing Collabo…
The Web Geometry Laboratory (WGL) is a collaborative and adaptive e-learning Web platform integrating a well known dynamic geometry system. Thousands of Geometric problems for Geometric Theorem Provers (TGTP) is a Web-based repository of…
The ongoing development of Lean 4's Mathlib has produced a macroscopic structural complexity that interweaves logical, mathematical, and infrastructural dependencies. We present a network analysis of this library, extracting its dependency…
Equation discovery is aimed at directly extracting physical laws from data and has emerged as a pivotal research domain. Previous methods based on symbolic mathematics have achieved substantial advancements, but often require the design of…
This paper considers the development of an AI-based provably-correct mathematical proof tutor. While Large Language Models (LLMs) allow seamless communication in natural language, they are error prone. Theorem provers such as Lean allow for…
This paper considers the development of an AI-based provably-correct mathematical proof tutor. While Large Language Models (LLMs) allow seamless communication in natural language, they are error prone. Theorem provers such as Lean allow for…
We introduce LeanConjecturer, a pipeline for automatically generating university-level mathematical conjectures in Lean 4 using Large Language Models (LLMs). Our hybrid approach combines rule-based context extraction with LLM-based theorem…
Computational and cognitive studies suggest that the abstraction of eventualities (activities, states, and events) is crucial for humans to understand daily eventualities. In this paper, we propose a scalable approach to model the…
Mathematical models and algorithms are an essential part of mathematical research data, as they are epistemically grounding numerical data. In order to represent models and algorithms as well as their relationship semantically to make this…
Automated theorem provers (ATPs) can disprove conjectures by saturating a set of clauses, but the resulting saturated sets are opaque certificates. In the unit equational fragment, a saturated set can in fact be read as a convergent rewrite…
The continuous growth of scientific literature brings innovations and, at the same time, raises new challenges. One of them is related to the fact that its analysis has become difficult due to the high volume of published papers for which…
Using AI to write formal proofs for mathematical problems is a challenging task that has seen some advancements in recent years. Automated systems such as Lean can verify the correctness of proofs written in formal language, yet writing the…
Trial-and-error is a fundamental strategy for humans to solve complex problems and a necessary capability for Artificial Intelligence (AI) systems operating in real-world environments. Although several trial-and-error AI techniques have…
Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and…
We give a simple approximation algorithm for a common generalization of many previously studied extensions of the maximum size stable matching problem with ties. These generalizations include the existence of critical vertices in the graph,…
Transport models are the main method to obtain physics information from low to relativistic-energy heavy-ion collisions. The Transport Model Evaluation Project (TMEP) has been pursued to test the robustness of transport model predictions in…
In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using…
The graph invariant EPT-sum has cropped up in several unrelated fields in later years: As an objective function for hierarchical clustering, as a more fine-grained version of the classical edge ranking problem, and, specifically when the…
Projected Entangled Pair States (PEPS) are a promising ansatz for the study of strongly correlated quantum many-body systems in two dimensions. But due to their high computational cost, developing and improving PEPS algorithms is necessary…
In structural proof theory, designing and working on large calculi make it difficult to get intuitions about each rule individually and as part of a whole system. We introduce two novel tools to help working on calculi using the approach of…
Proof assistants are computer softwares that allow us to write mathematical proofs so as to assess their correctness. In November 2021, I started the project of checking the simplicity of the alternating groups within the Lean theorem…