About the project

iProver Live

A browser-based interface for exploring and working with the iProver automated theorem prover.

About this web app

This web interface for iProver was developed by Maarij Khan under the supervision of Konstantin Korovin as a final-year undergraduate project at the University of Manchester in 2025–26.

The web app is available under the MIT License. This applies only to the web app; iProver's current license is available in its repository.

Comments and suggestions are welcome. Join the iProver Zulip chat or use the discussion and issue sections on the iProver GitLab page.

About iProver

Initially developed by Konstantin Korovin, iProver is an open-source automated theorem prover. It solves quantified first-order problems with theories and accepts the following formats:

TPTP — CNF, FOF and TFF0
SMT-LIB
QBF and DQBF — QDIMACS

This app provides an alternative to the command line, making iProver more approachable for professionals, researchers and enthusiasts working with automated theorem provers.