[Caml-list] ProoVer-2026: First Proof Verifier Competition

[geoff@cs.miami.edu]

ProoVer-2026: First Proof Verifier Competition
27th July 2026, Lisbon, Portugal
Co-located with CASC-J13 at IJCAR 2026 / FLoC 2026

We are pleased to announce ProoVer-2026, the first edition of the annual
competition for automatic proof verifiers. In ProoVer, verifiers are
given a mix of valid proofs and *evil* proofs in which tricky errors
have been deliberately introduced. The goal is to correctly identify
which proofs are valid and which are flawed.

Participants submit proof verifier systems that receive FOF (First-Order
Form) problems paired with TSTP-format proofs, and must determine
whether each proof is valid or flawed. For this first edition, only a
limited set of inference rules and formula roles will be used: `axiom`,
`conjecture`, `negated_conjecture`, as well as `plain` steps which
will be either skolemization steps or purely deductive steps whose
correctness can be delegated to an external ATP. What precisely makes a 
proof correct or incorrect will not be fully specified, and it is one 
of the main task  to handle edge cases and decide what should or should 
not be considered an acceptable proof according to the TSTP standard and 
general proof-checking principles.

Each system is evaluated on 100 problems: 50 valid proofs and 50 evil
proofs, with a time limit of 30 seconds per problem (wall-clock). The
output format is one SZS status line per problem, indicating whether the
proof is verified, failed, or uncertain. The competition infrastructure
is shared with CASC (StarExec).

IMPORTANT DATES (Anywhere on Earth)
------------------------------------
   System registration deadline   : 29th June 2026
   System descriptions deadline   : 13th July 2026
   Formal ProoVer registration    : 13th July 2026
   System delivery deadline       : 13th July 2026
   Competition start              : 10:00am, 27th July 2026

As ProoVer is held jointly with CASC, we will have a shared dinner and
if you participate in both competitions, registration fees are charged
only once (but you will get goodies for both! Great deal!).

For more information, please visit https://proover-competition.github.io/

The competition organizers are Julie Cailler and Simon Guilloud. If you
have any questions about the competition, please email us!