{"$schema":"https://json-schema.org/draft/2020-12/schema","$id":"https://assignee.net/schemas/math-result-v1","title":"Assignee Research Math Result","type":"object","required":["schema","schema_version","contract_version","publisher","result","verification","artifact_set","interpretation","limitations"],"properties":{"schema":{"const":"https://assignee.net/schemas/math-result-v1"},"schema_version":{"type":"string"},"contract_version":{"type":"string"},"schema_documentation":{"type":"string","format":"uri"},"changelog_url":{"type":"string","format":"uri"},"publisher":{"type":"object"},"result":{"type":"object"},"verification":{"type":"object","required":["state","label","proof_claim","n_cases","counterexample_available","lean4_source_public"],"properties":{"state":{"enum":["FALSIFIED","COMPUTATIONAL_EVIDENCE","FORMAL_PROOF_ATTEMPTED","FORMAL_PROOF_VERIFIED"]},"label":{"type":"string"},"proof_claim":{"type":"boolean"},"method":{"type":"string"},"result":{"type":"string"},"n_cases":{"type":"integer","minimum":0},"counterexample_available":{"type":"boolean"},"cpu_seconds":{"type":["number","null"]},"lean4_source_public":{"type":"boolean"}}},"artifact_set":{"type":"array","items":{"type":"object"}},"interpretation":{"type":"string"},"limitations":{"type":"array","items":{"type":"string"}}},"x-verification-states":[{"state":"FALSIFIED","label":"Falsified","definition":"A counterexample or failed verification condition is attached to the result record.","proof_claim":false},{"state":"COMPUTATIONAL_EVIDENCE","label":"Computational evidence","definition":"A bounded computation found no counterexample; this is not a proof.","proof_claim":false},{"state":"FORMAL_PROOF_ATTEMPTED","label":"Formal proof attempted","definition":"A formal proof attempt or proof report exists, but no public Lean4 source is attached.","proof_claim":false},{"state":"FORMAL_PROOF_VERIFIED","label":"Formal proof verified","definition":"A Lean4 proof source is publicly available for independent checking.","proof_claim":true}]}