The ProoVer 2026 competition will take place on 27 July 2026, as part of the FLoC Olympics held during FLoC 2026.
The infrastructure will be shared with CASC, and both competitions will run in parallel.
The competition setup and execution environment will follow the same principles as CASC.
We thank Geoff Sutcliffe for his support and for providing the competition infrastructure.

Deadlines and Important Dates (AoE)

  • System registration deadline: 29th June Online
  • System descriptions deadline: 13th July Email to Organizers
  • Formal ProoVer registration: 13th July Online
  • System delivery deadline: 13th July
  • CASC+ProoVer dinner: 25th July Rubro Campo Pequeno
  • Goodies distribution: At the CASC+ProoVer dinner
  • Start of competition: 10:30am, 27th July TBA
  • Trophy presentation: 28th July FLoC Banquet

Proceedings

The ProoVer 2026 proceedings are available here.

Results

Entrants

See here.

Problems and Proofs

The problems and proofs used for the ProoVer 2026 competition are available here.

Entrants’ System Descriptions

CheckProof 0.1

Nik Murzin
Wolfram Institute, USA

Overview

CheckProof 0.1 [Mur26] is a checker for first-order TSTP proofs. A proof is validated by replay: it is parsed into its sequence of annotated formulae, and each derived step is validated independently by dispatching on the inference rule that introduced it, so that one SZS status is reported for the whole proof [Sut08] Each rule carries a distinct obligation. An instantiate step is required to be a substitution instance of a parent; a negated_conjecture step to be the negation of its parent, checked by entailment in both directions so that a wrong quantifier dual is detected; a skolemize step to introduce a fresh Skolem symbol that occurs in the result; and a consequence, horn, or deduction step to be entailed by its parents. Entailment is decided by refutation with superposition, resolution, and paramodulation [BG94]: the parents and the negated conclusion are clausified and saturated, and a derived empty clause certifies the step. The refutation is required to close with the empty clause. Checking is conservative, in keeping with the scoring, under which a wrong verdict is penalised more heavily than abstention: a step is reported unsound only when a saturation is completed that exhibits a counter-model, and a step whose inference rule is not implemented, or whose entailment is neither proved nor refuted within the resource bound, leaves the proof unverified rather than guessed.

Implementation

CheckProof is implemented as a single self-contained C program, with no external dependencies beyond the C standard library. Proofs in TSTP syntax are read directly by a recursive-descent parser into the first-order term representation of the reasoning core. The obligations are discharged by FindProof's own clausal saturation engine, the same system entered in the CASC unit-equality division [Mur26]; no external prover is called, so equational atoms are reasoned about with superposition rather than treated as opaque. The checker is built from source by a single compiler invocation and is available from the author.

Expected Competition Performance

CheckProof is expected to be sound, accepting no invalid proof and rejecting no valid one, and to report a proof unverified when its steps use inference rules outside the implemented set or when an entailment cannot be settled within the time limit.

GAPT 2.20

Fabian Achammer
TU Wien, Austria

Overview

GAPT (General Architecture for Proof Theory) [EH+16] is a framework containing many data structures, algorithms, parsers and other components common in proof theory and automated deduction. As such it implements various proof calculi, including LK proofs and resolution proofs. The main idea of the GAPT proof checker is to attempt to import a given TSTP derivation as an acyclic directed graph of LK proofs which can then combined into a compact representation of an LK proof of a sequent whose antecedent contains input axioms and the negation of the input conjecture and whose succeedent contains $false. As a pre-pass GAPT performs other auxiliary checks like checking that the axiom file directives are correct. To check semantic entailment of plain inferences GAPT uses its internal superposition prover Escargot.

GAPT returns VerifiedBad if any of the checks fail, or any internal proof invariant is violated. If checking takes longer than the given time limit, GAPT returns Timeout. If an unexpected situation occurs (e.g., input syntax error, or unexpected exception thrown), GAPT returns Unknown. Otherwise, GAPT returns VerifiedGood. The checker not only outputs the SZS status, but in case of VerifiedBad it also gives a more detailed message as to what went wrong. For example, if Escargot can establish that a plain inference is incorrect, the checker outputs the step name of the incorrect inference.

The approach of importing the TSTP derivation as an LK proof allows, in principle, to compute a more elaborated version of the TSTP derivation that requires no external ATP tools to check anymore.

Implementation

GAPT is implemented in Scala. It uses parboiled2 as a parsing library to parse the TPTP format. The internal superposition prover Escargot is used for checking plain inferences, so GAPT does not depend on an external ATP tool for proof checking.

The proof checking proceeds in the following way: First the input file is parsed in the TPTP format. Then the file is checked for unique formula names and for acyclicity of the derivation. Next, auxiliary checks are performed to ensure all steps have valid statuses and the file directives in axioms and conjectures are correct. Now, each step is assigned a first-order sequent where the step's parents' formulas are in the antecedent and the step's formula is in the succeedent. For plain inference steps an attempt is made to find an LK proof for this sequent by using the internal superposition prover Escargot. For skolemization inference steps an LK proof for the sequent is constructed using a special skolemization LK rule. For negated conjecture steps an attempt is made to find an LK proof for both the if and only if direction of negation(conjecture) iff negated_conjecture. To make sure that skolem symbols are used appropriately across all inferences, e.g., the same skolem symbol is not used for different skolemized formulas, an additional check is performed across the whole derivation. Finally, for each step, LK cuts between the step's proofs and the step's parents' proofs are applied which results in LK proofs whose antecedents contain axioms and the negation of the conjecture from the input file and whose succeedent contains the formula of the given step. This results in a compact representation of the LK proof of the input refutation, i.e., an LK proof of the sequent whose antecedent consists of input axioms and the negation of the conjecture and whose succeedent consists of $false. This representation avoids unfolding the whole LK proof into a tree and instead saves space by remaining a directed acyclic graph.

GAPT is available at: 

    https://www.logic.at/gapt/

Expected Competition Performance

We expect GAPT to be sound, but as this is the first version of the GAPT derivation checker we don't expect fast results. It might struggle to verify long derivations or difficult plain inferences, since Escargot works very well on small examples, but is likely not able to compete with state-of-the art resolution provers in this area. However, GAPT should be able to handle most reasonably granular input derivations correctly and we expect to receive few negative points.

GDV 2.0

Geoff Sutcliffe
University of Miami, USA

Overview

GDV 2.0 [Sut06] is a verifier for derivations in classical first-order and typed first-order logic, written in the TPTP format. GDV checks a derivation in four verification phases: structural verification, leaf verification, rule-specific verification, and inference verification.

  • Structural verification deals with non-logical aspects of a proof, including checking the syntax, that formulae are uniquely named, the derivation is acyclic, refutations have false roots, etc.
  • Leaf verification ensures that the leaves of the derivation match formulae in the original input problem, and that introduced formulae such as definitions meet requirements.
  • Rule-specific verification deals with special cases, e.g., splitting as implemented in SPASS [Wei01]. Special techniques are available for verifying correctly documented Skolemization steps; see Section 2.3 of [SBB25].
  • Inference verification uses external trusted ATP systems to verify each inference step, based on the SZS status [Sut08] of the inference record. For example, inference steps often have the SZS status thm indicating that the inferred formula is (supposed to be) a theorem of the parent formulae. In this case a proof obligation with the parent formulae as the axioms and in the inferred formula as the conjecture is created, and discharged (or not) using a trusted theorem proving ATP system. Other SZS status values are treated with variants of that process.

Implementation

GDV is implemented in C. It is available from: 

    https://github.com/TPTPWorld/GDV

GDV relies heavily on the JJParser library, which has to be downloaded separately into the same directory as GDV: 

    https://github.com/TPTPWorld/JJParser

The external ATP systems run remotely, through the SystemOnTPTP service [Sut00].

Expected Competition Performance

The short time limit of 30s per proof, and the relatively slow process of running the remote ATP systems, means that GDV is likely to timeout often. GDV is sound, slow, but very sure of itself.

GDV-LP 2.0

Frédéric Blanqui
ENS Paris-Saclay, INRIA, France

Overview

GDV-LP 2.0 [SBB25] is a verifier for derivations in classical first-order and typed first-order logic, written in the TPTP format. GDV-LP checks a derivation in two steps:

  • Standard GDV (as described above) is run, using ZenonModulo [DD+13] as the trusted ATP system for discharging proof obligations. ZenonModulo is configured to output a LambdaPi term [HB20] for each discharge proof.
  • GDV-LP produces the necessary files that declare the formulae, the signatures of the symbols in the terms, a LambdaPi term for the root of the proof, and a lambdapi.pkg package file. ZenonModulo's LambdaPi terms are chained together from the root term, and passed to the lambdapi checker to be checked. The key strength of this added layer is that it is not necessary to trust the "trusted ATP system", here ZenonModulo. Additionally, tools other than lambdapi can be used to check the LambdaPi terms, e.g., dkcheck [Sai15] and kontroli [Far22].

Implementation

GDV-LP is implemented in C. It is available from: 

    https://github.com/TPTPWorld/GDV

GDV relies heavily on the JJParser library, which has to be downloaded separately into the same directory as GDV: 

    https://github.com/TPTPWorld/JJParser

ZenonModulo is implemented in OCaml. It is available from: 

    https://github.com/Deducteam/zenon_modulo

lambdapi is written in OCaml. It is available from: 

    https://github.com/Deducteam/lambdapi.git

ZenonModulo, other external ATP systems, and lambdapi run remotely, through the SystemOnTPTP service [Sut00].

Expected Competition Performance

The short time limit of 30s per proof, and the relatively slow process of running the remote ATP systems, means that GDV-LP is likely to timeout often, probably in the first non-LambdaPi step. GDV-LP is sound, slow, but very very sure of itself.

mrs-proover 0.2.0

Olivier Roland
Independent Researcher, France

Overview

mrs-proover 0.2.0 is a proof checker for TSTP first-order refutation proofs, built as a companion to the mrs automated theorem prover. It follows the semantic verification paradigm pioneered by GDV [Sut06]: structural properties of the proof DAG are checked first (uniqueness of formula names, acyclicity, a single $false root), followed by leaf verification against the linked problem file, followed by per-step verification of each inference.

A small set of inference patterns that are expected to recur in every proof — the negated-conjecture step, and Skolemization steps — are verified internally using dedicated structural checks rather than external provers, since these steps have precisely specified shapes (see the ProoVer Rules and Format page). Axiom and conjecture leaves are checked for alpha-equivalence against the named formula in the linked problem file, either internally or, when internal matching fails, by delegating to an external ATP. All other inference steps with status thm or cth are discharged as proof obligations to an ATP ladder.

mrs-proover reports Unknown (rather than guessing) whenever neither a positive nor a negative verdict can be established within the allotted resources for a given step; because the ProoVer scoring penalizes a false VerifiedGood on a bad proof ten times more heavily than a missed detection, the overall verdict policy is deliberately conservative: any single step found unsound anywhere in the proof yields VerifiedBad for the whole proof; otherwise any step left undecided yields Unknown; only if every step is positively confirmed does the proof yield VerifiedGood.

Implementation

mrs-proover is implemented in Rust (edition 2024), reusing the mrs TPTP/TSTP parser, clausifier, and unification/formula-lowering crates from the same workspace. The proof is loaded and its dependency structure is represented as a directed acyclic graph over annotated formulae; formulae are lowered from the TPTP AST into the shared mrs-core term/formula representation for alpha-equivalence and structural comparisons. For inference steps that cannot be settled by the internal structural checks, mrs-proover discharges the corresponding proof obligation (parent formulae as axioms, inferred formula as conjecture) to an ATP ladder that runs, per step, the in-process mrs prover first, then races any available external backends — E [Sch02] and Vampire [KV13] — in parallel; the first definite Sound/Unsound verdict from any ladder member wins and the remaining subprocesses for that step are cancelled. Steps can be verified concurrently across multiple CPU cores (default 8, matching the competition hardware).

mrs-proover has been cross-checked, using only its internal mrs backend (no external ATPs), against the 7 official ProoVer example proofs, against the leoprover/noergler PyRes correctness corpus (170 valid proofs, 170 corresponding falsified/mutated proofs), and against the ATP-Research-Project test corpus of correct and deliberately "evil" proofs. Across all of these, running the in-process backend alone never produced a false VerifiedGood on an evil proof and never produced a false VerifiedBad on a valid proof; adding the external E/Vampire backends only improves detection rate (fewer proofs left at Unknown), never soundness.

mrs-proover is open source (MIT OR Apache-2.0) and available from: 

    https://github.com/newca12/mrs

as the mrs-proover crate in the same repository as the mrs ATP system.

Expected Competition Performance

mrs-proover is expected to correctly identify almost all well-formed valid proofs as VerifiedGood and almost all deliberately incorrect ("evil") proofs as VerifiedBad, given the internal structural checks tailored to the exact Skolemization and negated-conjecture formats specified by the ProoVer rules, backed by external ATP calls for the remaining steps. Given the highly asymmetric scoring (a single false Verified on an evil proof costs as much as ten correct verifications), mrs-proover is tuned to prefer reporting Unknown over guessing whenever a step cannot be positively confirmed or refuted within the time budget, so a non-trivial fraction of harder or unusually-shaped valid proofs may be conservatively scored 0 rather than +1.

Nörgler 1.1

Alexander Steen
University of Greifswald, Germany

Overview

The proof checker Nörgler 1.1 [TSS26, STS26] is designed as a light-weight system for the verification of TSTP refutations across various logic dialects, including propositional, untyped or typed first-order, and higher-order logics. The architecture is built upon the semantic verification paradigm pioneered by the GDV system [Sut06]. This approach combines structural property verification using dedicated checks with the verification of individual proof steps by re-proving each inference using trusted general-purpose automated theorem provers. A core design choice in the system is the integration of multi-core parallelization, which allows independent proof checking tasks to be processed concurrently, thereby significantly increasing performance and reducing overall verification time.

The verification process is executed via a multi-stage checking strategy. Initially, global structural properties of the proof (such as ensuring the proof graph is acyclic, verifying that formula names are unique, and confirming that the derivation correctly terminates in false) are validated. Following these global assessments, individual logical inferences are evaluated. This comprises checks of local structural properties (such as ensuring that a given step has an appropriate TSTP role and that all listed parents exist earlier in the proof) and the semantical verification of the inferences. Nörgler checks the faithfulness of all formulae taken from the problem file. With the exception of the negation of the conjecture and Skolemisazation, which are verified by dedicated checks, the inferences are verified by invoking an external trusted prover. If this check does not succeed within the allocated resource limit, countermodel search is invoked via integrated model finders to actively detect incorrect proof steps. If a countermodel is found, the inference is rejected as invalid (resulting in a VerifiedBad status); however, if neither a successful proof nor a definitive countermodel can be established by the auxiliary tools, a status of Unknown is reported. If all checks are successful, Nörgler returns VerifiedGood.

Several notable features are incorporated into the system to enhance its flexibility and robustness. Fine-grained control over the strictness with which formatting conventions are enforced is provided, enabling the system to either gracefully handle imperfect prover outputs or strictly demand adherence to proof standards, see [TSS26] for details.

Implementation

Nörgler is implemented in Scala, making use of its native support for concurrency via Futures and functional data structures. The system incorporates the scala-tptp-parser library [Ste26] for robust parsing of the standard TPTP/TSTP grammar formats, and integrates the tptp-utils tool for formula manipulation [Ste25]. For its backend verification tasks, the well-known systems E [Sch02] and Mace4 [McC03] (for proving resp. disproving) are used. The system is freely available as open-source software (MIT license), and can be accessed online via its repository at GitHub: 

    https://github.com/leoprover/noergler/

Expected Competition Performance

This is the very first version of Nörgler, so no reliable expectations can be formulated. The author's are positive, however, that Nörgler should not report false positives (i.e., reporting a successful verification on a flawed proof).

ProofCheck 1.0

Jeff Machado
Independent Researcher, USA

Overview

ProofCheck 1.0 is a verifier for first-order refutation proofs written in the TPTP format. A proof is checked by structural verification followed by independent verification of every inference step, and is reported as VerifiedGood, VerifiedBad, Unknown, or Timeout. The verifier has a single, strict mode: by construction, no derived step can be accepted without verification, and a step that cannot be decided is reported as Unknown rather than VerifiedGood, to avoid false acceptance.

Structural verification checks the syntax, unique naming, acyclicity, a $false root, and that the leaves match the input problem (located from the proof's % Proof : header). Leaf bodies are compared against their cited problem formulae canonically, with an ATP equivalence check as the fallback, and clausal leaves are validated by replaying the clausification of their source formula. Introduced definitions are checked for conservativity and Skolem-symbol laundering.

Inference verification discharges every thm and cth step by an ATP proof obligation built from exactly that step and its cited premises: the parents as axioms and the conclusion as conjecture, discharged by a local E [SCV19] raced against Mace4 [ML26], where a Mace4 countermodel refutes the step; a step that E leaves undecided is retried with Vampire [KV13] as a second entailment oracle before the step is hedged. SideStep, a built-in clausal inference engine, replays clausal steps structurally in process first; a step it refutes is rejected outright, while its acceptances are not trusted and the step still goes to the ATP. Skolemization (esa) steps are never sent to an ATP; they are verified structurally against the parent: the required skolemize(Var,Term) record, the Skolem term's arguments against the universally quantified variables in scope at the eliminated existential, symbol freshness across the proof and against the problem's own symbols, and one fresh symbol per eliminated (non-vacuous) existential. Constructs outside the specification are hedged to Unknown. A wall-clock deadline is self-imposed, so one of the four verdicts is always emitted within the time budget.

Implementation

ProofCheck is implemented in C++, including the SideStep engine and the structural checkers. It compiles into a single static binary that invokes E [SCV19] and Vampire [KV13] as entailment provers, Mace4 [ML26], as the countermodel finder, and Prover9 [ML26], for clausification replay, all locally from the directory of the binary. It is available from: 

    https://github.com/AlgorithmicTruth/proofcheck-releases

Expected Competition Performance

The entailment backends are local and most structural checks are in process, so ProofCheck verifies typical proofs in well under a second and rarely times out. It has been tested for soundness on an adversarial library of over 200 red-team proofs, a third-party evil proof suite, and several hundred mutated E proofs, with no false VerifiedGood observed, and for coverage on several hundred valid E and Prover9 proofs. Constructs the verifier does not model are reported as Unknown rather than accepted, so unanticipated cases reduce coverage, not soundness. ProofCheck is sound and fast.

ProofGuard 1.0

Matthew Farah
McMaster University, Canada

Overview

ProofGuard 1.0 is an automatic checker for first-order logic proof certificates submitted in the TSTP format [Sut24]. A problem file and a proposed proof file are taken as input, and it is checked whether the proof establishes the claimed contradiction. The system is designed for refutation proofs. A proof is accepted only when every step of the argument can be followed and it can be confirmed that $false is correctly derived. When all required steps have been verified, the proof is reported as verified.

ProofGuard is intentionally conservative. When a proof step is unclear, unsupported, malformed, or cannot be checked within the available time, no guess is made. It is instead reported that the proof could not be verified. A proof is rejected as flawed only when a definite error can be identified, such as an incorrect negated conjecture, an invalid Skolemization step, or an inference which does not follow from its stated premises. This design reflects the competition setting, in which the incorrect acceptance of a bad proof is heavily penalized. Caution is therefore prioritized, wherein only fully checked proofs are accepted, only demonstrably flawed proofs are rejected, and verification is otherwise reported as inconclusive.

Verdicts are reported using the required SZS statuses [Sut08]. An accepted proof is reported as VerifiedGood; a rejected proof is reported as VerifiedBad, together with a one-line reason naming the flawed step; an inconclusive verification is reported as Unknown; and an exhausted time budget is reported as Timeout.

Implementation

ProofGuard 1.0 (July 2026) is the first release of the system. The E prover, built from current upstream sources, is bundled with the system as the backend ATP.

  • Problem and proof parsing. FOF problem files and TSTP proof files are parsed by a recursive-descent parser, and formulas are represented as immutable dataclass terms. Nested inference(...) chains are flattened to their leaf premises.
  • Input-step validation. Steps imported from the problem file are checked against the referenced problem formula, modulo alpha-renaming and harmless syntactic normalizations such as literal order and equation orientation.
  • Internal rule checking. Specified rules are verified internally. Negated-conjecture steps are checked against the negation of the original conjecture, which may be consumed by no other step. Skolemization steps are checked for fresh Skolem symbols, consistent annotations, and correct dependency on the universal variables in scope.
  • Conservative de-Skolemization fallback. When Skolemization annotations are absent, de-Skolemization is attempted only when the transformation is unambiguous: each fresh Skolem term is replaced by a new existentially bound variable, after which the remaining theorem-status content is checked by the ATP. Whenever the transformation cannot be performed unambiguously, verification is reported as inconclusive.
  • ATP-backed consequence checking. Unspecified inference steps marked with theorem status are checked through the generation of local proof obligations for the E prover [SCV19]. The original conjecture is never independently re-proved.
  • Conservative failure policy. A demonstrably incorrect step causes a failed verification to be reported. A malformed, unsupported, ambiguous, timed-out, or internally failing check causes verification to be reported as inconclusive; the system is never crashed by malformed input.
  • Resource management. A global wall-clock budget is managed by the checker. Each ATP call is given a CPU limit derived from the remaining time, and the system is terminated conservatively before the external time limit is exceeded.
  • Packaging and reproducibility. ProofGuard is implemented in pure Python 3 with no third-party Python libraries. The delivery package is built with Docker and is fully self-contained: the CPython runtime, the E binary, and the checker are all included, glibc 2.17 is targeted, and the system is launched as ./proover-check PROBLEM PROOF.
  • Testing. The system was tested on the published ProoVer examples, on E-generated TSTP proofs over the TPTP library, on multi-system TSTP samples, and on mutation-fuzzed proof variants.

The source is available here: 

    https://github.com/ValueAchooMatthew/ATP-Research-Project

Expected Competition Performance

All published example problems are classified correctly, and each evil proof is rejected for its intended flaw. Wrong answers are expected to be rare: across 58 TSTP proofs produced by five different systems, no correct proof was misclassified as flawed, and no mutation-fuzzed proof was ever accepted. The strongest performance is expected on invalid proofs, for which structural checks and countersatisfiability results are obtained cheaply and definitively. On the published 8 MB stress sample, a flaw (a missing Skolem dependency at step 219 of 223) is located in roughly 12 seconds, without any ATP call on the large formulas. Valid proofs written in the style of the published examples are expected to be verified within the time limit, while proofs relying on techniques outside the system’s coverage are reported as inconclusive rather than risked. Overall, it is expected that most lost points will be attributable to inconclusive verdicts rather than to penalties.

PyCheck 0.1

Stephan Schulz
DHBW Stuttgart, Germany

Overview

PyCheck is a simple (mostly) semantic proof checker for refutation-based proofs in the most commonly used subset of TPTP/TSTP CNF/FOF syntax. Inspired by GDV [Sut06], it performs both structural and semantic checks on proof files. Among the structural checks are existance of an explicit contradiction, acyclicity of the proof graph, and freshness of introduced (Skolem) symbols. Semantic checks include verification of "status(thm)" and "status(cth)" checks using the external prover.

Implementation

PyCheck reuses the parser and a lot of internal data structures from PyRes [SP20], and thus supports the same core of the TPTP-3 proof language, with support added for more detailed derivations.

PyCheck calls an external prover (usually E [SCV19]) to verify most proof steps (in particularly those with thm and cth semantics). It uses internal processing to try to verify Skolemization steps, to check existence of axioms in the original input file, and to perform structural checks on the proof graph.

PyCheck can be downloaded from GitHub: 

    https://github.com/eprover/PyCheck

It requires E (https://www.eprover.org) to be available in its search path (the ProoVer StaExec package should automatically do everything necessary).

Expected Competition Performance

PyCheck 0.1 is at a very early state of maturity. It can handle all the problems given in the ProoVer description, but may fail to catch some particulary malicious structural problems of proofs. Overall, it should prove to be at least useful.

VaLeaDate 0.1

Jonas Bodingbauer
TU Wien, Austria

Overview

VaLeaDate v0.1 is a proof verification system for TPTP proofs. It leverages a recently developed proof output from Vampire, which generates proofs as Lean input files that are end-to-end verifiable by Lean [BH26]. The core approach of VaLeaDate is to invoke Vampire on each inference, inspired by GDV [Sut06], chain the resulting proof steps together, and subsequently verify the entire proof in Lean. Since the proof checking step is time-consuming, VaLeaDate checks multiple structural properties of the proof in the beginning and terminates early if any of these checks fail. These basic checks include:

  • Verifying that all parent nodes exist
  • Checking for acyclicity of the proof structure
  • Ensuring axioms are alpha-equivalent to the problem input

After that, all inferences are passed to the ATP Vampire, which processes them in a parallelized manner. The resulting proof steps are then chained together (in one or multiple files depending on the size of the proof output) and verified by Lean. Skolemization is handled within VaLeaDate, generating a skolemization section in the Lean proof output, which is then verified by Lean. The process transforms any input into NNF, skolemizes it, and then reconstructs it (if necessary) back to the expected form.

The system reports status Unknown for (some) syntactic errors or if Vampire does not produce a conclusive result (neither satisfiable nor a refutation). VerifiedBad is produced if any of the basic checks fail or if the Lean verification fails. Finally, VerifiedGood is produced if all checks pass and the final Lean verification also succeeds.

Implementation

VaLeaDate is implemented in Scala and utilizes the scala-tptp-parser parser from the leoprover project to parse TPTP input and proof files. Furthermore, it relies on Lean, a small Lean library VampLean, as well as a custom Vampire build configured for proof output (including VaLeaDate-specific functions). It aims to parallelize the computationally intensive parts of proof reconstruction and verification as much as possible.

Expected Competition Performance

It is challenging to predict the performance, but it is hoped that VaLeaDate does not produce any false positives. They can still occur due to the somewhat open definition of correctness or other bugs introduced during the relatively short development period. Since verification in Lean introduces some overhead, the system might time out on many problems within the given 30s time limit.