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! _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
