Mathematical Proofs

Benchmarks archive 2025-07-28

No benchmark for this task in the archive.

Libraries

Not in the archive: the export carries no per-task library table, so there is nothing to show at snapshot 2025-07-28.

Datasets archive 2025-07-28

3 datasets whose archive record lists this task, ordered by the archive's paper count.

Subtasks archive 2025-07-28

1 subtask in the archive's task tree.

Most implemented papers archive 2025-07-28

29 shown of 29 papers with code (90 tagged with this task in all), ordered by repositories listed in the archive, not by stars (the archive holds no stars, so PwC's “Social” and “Latest” sorts cannot be reproduced). Papers without a page here are shown as plain text.

• BreastScreening: On the Use of Multi-Modality in Medical Imaging Diagnosis
  7 Apr 2020 8 repositories listed
  This paper describes the field research, design and comparative deployment of a multimodal medical imaging user interface for breast screening.
• Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs
  21 Oct 2022 3 repositories listed
  In this work, we introduce Draft, Sketch, and Prove (DSP), a method that maps informal proofs to formal proof sketches, and uses the sketches to guide an automated prover by directing its search to easier sub-problems.
• TransERR: Translation-based Knowledge Graph Embedding via Efficient Relation Rotation
  26 Jun 2023 2 repositories listed
  This paper presents a translation-based knowledge geraph embedding method via efficient relation rotation (TransERR), a straightforward yet effective alternative to traditional translation-based knowledge graph…
• IsarStep: a Benchmark for High-level Mathematical Reasoning
  13 Jun 2020 2 repositories listed Syntology ran 2 of 8 samples · 6 unverified
  In this paper, we present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models.
• AdaSwarm: Augmenting Gradient-Based optimizers in Deep Learning with Swarm Intelligence
  19 May 2020 2 repositories listed
  This paper introduces AdaSwarm, a novel gradient-free optimizer which has similar or even better performance than the Adam optimizer adopted in neural networks.
• StepProof: Step-by-step verification of natural language mathematical proofs
  12 Jun 2025 1 repository listed
  Recent advancements in large language models (LLMs) have enhanced the understanding of natural language inputs, paving the way for autoformalization - the process of translating natural language proofs into formal…
• A Theoretical Analysis of Compositional Generalization in Neural Networks: A Necessary and Sufficient Condition
  5 May 2025 1 repository listed
  This paper derives a necessary and sufficient condition for compositional generalization in neural networks.
• Hierarchical Attention Generates Better Proofs
  27 Apr 2025 1 repository listed
  Large language models (LLMs) have shown promise in formal theorem proving, but their token-level processing often fails to capture the inherent hierarchical nature of mathematical proofs.
• Distance-Adaptive Quaternion Knowledge Graph Embedding with Bidirectional Rotation
  5 Dec 2024 1 repository listed
  Our model combines semantic matching with entity's geometric distance to better measure the plausibility of triplets.
• Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
  2 Nov 2024 1 repository listed
  Formally verifying the correctness of mathematical proofs is more accessible than ever, however, the learning curve remains steep for many of the state-of-the-art interactive theorem provers (ITP).
• ODGS: 3D Scene Reconstruction from Omnidirectional Images with 3D Gaussian Splattings
  28 Oct 2024 1 repository listed
  In this work, we present ODGS, a novel rasterization pipeline for omnidirectional images, with geometric interpretation.
• FormalAlign: Automated Alignment Evaluation for Autoformalization
  14 Oct 2024 1 repository listed Syntology ran 3 of 3 samples · 0 unverified · 3 pointer-only (licence)
  To address this, we introduce \textsc{FormalAlign}, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization.
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
  9 Sep 2024 1 repository listed
  Formalizing mathematical proofs using computerized verification languages like Lean 4 has the potential to significantly impact the field of mathematics, it offers prominent capabilities for advancing mathematical…
• Simple but Effective Compound Geometric Operations for Temporal Knowledge Graph Completion
  13 Aug 2024 1 repository listed
  Temporal knowledge graph completion aims to infer the missing facts in temporal knowledge graphs.
• SciEx: Benchmarking Large Language Models on Scientific Exams with Human Expert Grading and Automatic Grading
  14 Jun 2024 1 repository listed
  We evaluate the performance of various state-of-the-art LLMs on our new benchmark.
• A New Approach Towards Autoformalization
  12 Oct 2023 1 repository listed
  This is a challenging task, and especially for higher-level mathematics found in research papers.
• GENTLE: A Genre-Diverse Multilayer Challenge Set for English NLP and Linguistic Evaluation
  3 Jun 2023 1 repository listed
  We evaluate state-of-the-art NLP systems on GENTLE and find severe degradation for at least some genres in their performance on all tasks, which indicates GENTLE's utility as an evaluation dataset for NLP systems.
• A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification
  24 May 2023 1 repository listed
  Initially, we employ Bounded Model Checking (BMC) to identify vulnerabilities and extract counterexamples.
• Sharpness-Aware Minimization Alone can Improve Adversarial Robustness
  9 May 2023 1 repository listed
  In this paper, we explore SAM in the context of adversarial robustness.
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
  5 Jan 2023 1 repository listed Syntology ran 0 of 7 samples · 7 unverified
  The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding.
• Formal Development of Safe Automated Driving using Differential Dynamic Logic
  14 Apr 2022 1 repository listed
  The challenges in providing convincing arguments for safe and correct behavior of automated driving (AD) systems have so far hindered their widespread commercial deployment.
• Calibration of P-values for calibration and for deviation of a subpopulation from the full population
  31 Jan 2022 1 repository listed Syntology ran 1 of 3 samples · 2 unverified
  The author's recent research papers, "Cumulative deviation of a subpopulation from the full population" and "A graphical method of cumulative differences between two subpopulations" (both published in volume 8 of…
• Theory-guided hard constraint projection (HCP): a knowledge-based data-driven scientific machine learning method
  11 Dec 2020 1 repository listed
  Machine learning models have been successfully used in many scientific and engineering fields.
• Differential Machine Learning
  5 May 2020 1 repository listed
  It is also applicable in many situations outside finance, where high quality first-order derivatives wrt training inputs are available.
• Epistemic Phase Transitions in Mathematical Proofs
  31 Mar 2020 1 repository listed
  Mathematical proofs are both paradigms of certainty and some of the most explicitly-justified arguments that we have in the cultural record.
• Learning to Prove Theorems via Interacting with Proof Assistants
  21 May 2019 1 repository listed
  Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics.
• α-Rank: Multi-Agent Evaluation by Evolution
  4 Mar 2019 1 repository listed
  We introduce {\alpha}-Rank, a principled evolutionary dynamics methodology, for the evaluation and ranking of agents in large-scale multi-agent interactions, grounded in a novel dynamical game-theoretic solution concept…
• A Unified Parallel Algorithm for Regularized Group PLS Scalable to Big Data
  23 Feb 2017 1 repository listed
  Partial Least Squares (PLS) methods have been heavily exploited to analyse the association between two blocs of data.
• Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
  17 Aug 2011 1 repository listed
  A good method for premise selection in complex mathematical libraries is the application of machine learning to large corpora of proofs.

Syntology lines on 4 of the papers shown; no Syntology record for the others (a paper without an arXiv id cannot be joined to the graph, and absence from the graph layer is not a recorded non-run). “Ran” means the sample executed on a synthesized fixture, not that the paper's result was reproduced. Read from the graph 2026-09-24.