The SPRIG Protocol is a new protocol allowing anyone to know why a mathematical reasoning is valid, and enabling anyone to ask questions in case of doubt. We are part of the Algorand Foundation Grant Awardees, and building the SPRIG Platform on the Algorand blockchain.

(July 20, 2022) We are excited to announce that the Algorand Foundation has unlocked the second wave of funding of the SPRIG project, following the completion of the centralized test version of the protocol. We now began working on the smart contracts to deploy SPRIG on the blockchain.

(June 17, 2022) A centralized test version of the SPRIG protocol has been completed !

(Nov. 2021) We are happy to announce that SPRIG received funding from the Algorand Foundation!

Proofs connect statements with one another, building elaborated assertions upon elementary ones

... but how do we know the chain of deductions is complete?

The validity of a proof is often based on the aggregation of the views of few researchers

The current system allows one to deal with concise and informative proofs, at the expense of a lower level of trust

Mathematical formalization and proof verification system would allow one for systematic verification of proofs

Yet, formal proofs are generally prohibitively time-consuming to produce and are not "smart": not all details are equally interesting, and only a few specific points are really nontrivial and informative

The SPRIG protocol leverages the best of both worlds by allowing agents to debate on proofs and to use a machine-level verification system to settle persisting disagreements

The SPRIG protocol is introduced in the 2021 whitepaper by S. Carré, F. Gabriel, C. Hongler, G. Lacerda, and G. Capano

New mechanisms to communicate results and their proofs

A way to question any statement, to request a deeper answer of why it is true

A way to elaborate proofs that are of interest to the community

A mechanism to signal weaknesses in proofs and be rewarded

The SPRIG Protocol is a new mechanism for proof validation, which yields efficient proofs via recursive debates on the statements appended to the SPRIG tree

Proofs are trees: for any statement, a claim of proof consists of a list of sub-statements, which themselves can be questioned and proven

The lowest-level leaves of the tree (i.e. the statements that cannot be further questioned) consist of machine-level proofs, i.e. sequences of statements that can be verified by a computer

The SPRIG tree grows with questions and answers:

For any claim of proof, a skeptic can question one of its statements, by locking a bounty, to be awarded to the first agent providing a valid proof

For any question, a prover can provide a claim of proof, consisting of a sequence of statements, by locking a stake which will be released to the first agent who finds a flaw in it

In case of persisting disagreements, proofs must reach (within a fixed number of steps) the machine level, where they are settled automatically

A skeptic who finds a statement that cannot be proven (within a given timeframe) is awarded the corresponding locked stake

A prover who provides a proof for a statement that cannot be invalidated (within a given timeframe) is awarded the associated bounty

Skeptics should only ask questions about statements that they believe may lack a proof; provers should only publish proofs for which they believe that all details can be provided

As discussed in the whitepaper, SPRIG proofs are resilient against various types of attacks from actors acting in bad faith

The SPRIG protocol is designed in a way that allows for complete decentralization, and is naturally designed to be run on the blockchain

The protocol can be run autonomously as a smart contract on a blockchain, that locks stakes and bounties, and awards them to the relevant parties

Machine-level proofs are automatically settled, either by on-chain or by off-chain solutions

All the proofs and the associated interactions are transparently available on the blockchain, bringing information about which parts of the proofs are deemed non-trivial, and enhancing the trust in the verification process

The SPRIG Platform aims at enabling users to prove, submit, and question mathematical statements in an intuitive and secure way

The SPRIG Platform will allow all users to navigate through the SPRIG Forest (the set of all the proof trees) as it grows in real time, and to gain maximally useful information about statements as they get published and verified

The SPRIG Platform will enable users to question the validity of a proof step, or to provide an answer to a question and to be compensated for their useful work

With SPRIG, anyone can publish a proof, with a stake, serving as reviewing fee, which will incentivize agents to find flaws in the steps

With SPRIG, anyone can create a challenge, awarding a bounty to prove a statement, which will generate a tree of proof proposals that will be debated by the community of agents

The trust in the proofs that are validated is established by the fact that any agent able to identify a problem is incentivized to signal it

The presence of a proof on the blockchain for a long enough period of time is thus a guarantee that no one is able to identify a problem in it

The SPRIG Association was founded in 2021 with the aim of heralding the SPRIG vision through the development of the SPRIG platform

The Association aims at fostering the implementation of the SPRIG vision, as well as at further developing its theoretical foundations and extending its scope

Clément Hongler is a Swiss mathematician, known for works in mathematical physics, probability, and machine learning theory. He leads the Chair of Statistical Field Theory at EPFL. He has also worked in various creative digital projects, and has founded Quine, a non-profit organization dedicated to research in artificial life and blockchain questions, and to dissemination of scientific knowledge

Franck Gabriel is a French mathematician, working in probability, mathematical physics, economics, and machine learning theory at EPFL. He is known for recent works in Deep Learning (in particular, with the discovery of the Neural Tangent Kernel describing the Deep Neural Net dynamics) and is a co-founder of Quine

Sylvain Carré is a French economist, working mainly on the theory of Financial Intermediation (TradFi and DeFi), using game-theoretic approaches. He is currently working as an Assistant Professor at the Economics Department of Université Paris-Dauphine

Diego Dorn is a French MSc student in mathematics and computer science at EPFL. His main interests are programming languages, formal proofs, game theory and decentralised systems. He is the co-creator of the esoteric programming language AsciiDots

Yann Aguettaz is a French MSc student in computer science, enrolled in a joint degree at EPFL and ENS Lyon. He is particularly interested in cryptography and privacy-preserving technologies, quantum computing, formal verification and diffusion of knowledge.

Christophe Nussbaumer has served as a project manager for various non-profit organizations. He obtained a master’s degree in public management and policy at UNIL. He is passionate about technology and everything related to distributed ledgers. He also co-founded Quine