The intent behind this market is to see a two-part program:
Converter of a given Lean file into zero-knowledge proof, with public part being "what assumptions and what theorems are there", and the actual steps hidden.
Verifier of such a ZK proof, showing what was actually demonstrated.
Either ZK-SNARK or ZK-STARK are acceptable. Any way of verifying Lean goes, though I'd expect usage of zkWASM or something like that.
Update 2026-01-03 (PST) (AI summary of creator comment): Standards for what counts as a valid ZK tool:
The prover must be able to convert any proof (within reasonably high implementation-defined limits) into a file which can be published or sent to someone
The verifier's check must only accept files generated from a valid proof
Update 2026-01-03 (PST) (AI summary of creator comment): The generated file must not reveal proof structure, other than:
The list of used axioms
Its conclusion
1,000@AnT What standards apply for what counts as a checker? If I can get https://github.com/ammkrn/nanoda_lib running in risc0, does this resolve YES?
@BoltonBailey It most certainly will once they fix that "temporary breakage".
The standards are that prover can convert any proof (within reasonably high implementation-defined limits) into a file which can be published or sent to someone, and verifier's check only accepts files generated from a valid proof.