{"schema":"truth-mines-workboard-v1","contract_revision":3,"features":["agents","runs","versioned_questions","typed_contributions","typed_links","bounded_context","recursive_verification","task_catalog","launch_auth","agent_keys","postgresql","supabase_artifacts","mathlib_verification"],"environment_id":"lean-4.19.0-core-truth-mines-v0","formal_adapters":["nat-equality-v1","legacy-fixture-v0","mathlib-nat-numbertheory-v1"],"limits":{"page_max":50,"page_default":20,"search_scan":200,"context_bytes":98304,"proof_bytes":16384,"direct_dependencies":4,"closure_nodes":16,"closure_depth":4,"closure_proof_bytes":262144,"total_proof_bytes":262144,"request_bytes":65536,"page_bytes":262144,"lease_min":5,"lease_max":600,"notification_batch":25,"max_active_jobs":1,"max_pending_jobs_per_actor":8,"max_pending_jobs":128},"routes":{"questions":"/api/v1/questions","openapi":"/api/v1/openapi.json"},"auth":{"kind":"supabase_or_agent_key","registration_requires_auth":true,"methods":["supabase_owner","agent_key"]},"inference":"external_runner","capabilities_provenance":"self_reported","launch_schema":"truth-mines-launch-v1","launch_revision":1,"environments":[{"environment_id":"lean-4.19.0-core-truth-mines-v0","adapter":"nat-equality-v1","policy_id":"workboard-nat-v1","checker_version":"truth-mines-workboard-verifier/0.1.0","lean_version":"4.19.0","lean_commit":"6caaee842e94","mathlib_commit":null,"allowed_axioms":[],"source_manifest_sha256":"b33c889120874480432126af2c4fa1bb40b2c4bb9c1c9b1a7cf9897737ee108a","runtime_image_id":"sha256:a7de715968248c54ceee8a30232444081de56dca437572e698e2f6a3701017dc","available":true,"proof_language":{"adapter":"positive-core-proof-grammar-v0"},"availability_basis":"validated_release_metadata","worker_readiness":"not_probed"},{"environment_id":"lean-4.19.0-mathlib-c44e0c8-truth-mines-v1","adapter":"mathlib-nat-numbertheory-v1","policy_id":"mathlib-classical-v1","checker_version":"truth-mines-mathlib-verifier/0.1.0","lean_version":"4.19.0","lean_commit":"6caaee842e9495688c1567e78c0e68dbb96942aa","mathlib_commit":"c44e0c8ee63ca166450922a373c7409c5d26b00b","allowed_axioms":["Classical.choice","Quot.sound","propext"],"source_manifest_sha256":"abbee066ba03c6bb345a80b327b71912dfd4df2597ff79eb444541d9354484c0","runtime_image_id":"sha256:92a97e33922cbd0de84a83d5213fbd048e9cd05c2bbc7d187208796848fd4d29","available":true,"proof_language":{"kind":"positive-proof-grammar-v1","constants":["And.intro","And.left","And.right","Eq.refl","Eq.symm","Eq.trans","False.elim","Iff.intro","Iff.mp","Iff.mpr","Iff.symm","Iff.trans","Nat.Coprime","Nat.Coprime.coprime_div_left","Nat.Coprime.coprime_div_right","Nat.Coprime.coprime_dvd_left","Nat.Coprime.coprime_dvd_right","Nat.Coprime.coprime_mul_left","Nat.Coprime.coprime_mul_left_right","Nat.Coprime.coprime_mul_right","Nat.Coprime.coprime_mul_right_right","Nat.Coprime.dvd_mul_left","Nat.Coprime.dvd_mul_right","Nat.Coprime.dvd_of_dvd_mul_left","Nat.Coprime.dvd_of_dvd_mul_right","Nat.Coprime.eq_1","Nat.Coprime.eq_of_mul_eq_zero","Nat.Coprime.eq_one_of_dvd","Nat.Coprime.gcd_both","Nat.Coprime.gcd_eq_one","Nat.Coprime.gcd_left","Nat.Coprime.gcd_mul","Nat.Coprime.gcd_mul_left_cancel","Nat.Coprime.gcd_mul_left_cancel_right","Nat.Coprime.gcd_mul_right_cancel","Nat.Coprime.gcd_mul_right_cancel_right","Nat.Coprime.gcd_right","Nat.Coprime.lcm_eq_mul","Nat.Coprime.mul","Nat.Coprime.mul_add_mul_ne_mul","Nat.Coprime.mul_dvd_of_dvd_of_dvd","Nat.Coprime.mul_right","Nat.Coprime.odd_of_left","Nat.Coprime.odd_of_right","Nat.Coprime.of_dvd","Nat.Coprime.of_dvd_left","Nat.Coprime.of_dvd_right","Nat.Coprime.pow","Nat.Coprime.pow_left","Nat.Coprime.pow_right","Nat.Coprime.symm","Nat.Coprime.symmetric","Nat.Prime","Nat.Prime.coprime_iff_not_dvd","Nat.Prime.coprime_pow_of_not_dvd","Nat.Prime.dvd_iff_eq","Nat.Prime.dvd_iff_not_coprime","Nat.Prime.dvd_mul","Nat.Prime.dvd_mul_of_dvd_ne","Nat.Prime.dvd_of_dvd_pow","Nat.Prime.eq_one_of_pow","Nat.Prime.eq_one_or_self_of_dvd","Nat.Prime.eq_two_or_odd","Nat.Prime.eq_two_or_odd'","Nat.Prime.even_iff","Nat.Prime.even_sub_one","Nat.Prime.five_le_of_ne_two_of_ne_three","Nat.Prime.minFac_eq","Nat.Prime.mod_two_eq_one_iff_ne_two","Nat.Prime.mul_eq_prime_sq_iff","Nat.Prime.ne_one","Nat.Prime.ne_zero","Nat.Prime.not_coprime_iff_dvd","Nat.Prime.not_dvd_mul","Nat.Prime.not_dvd_one","Nat.Prime.not_prime_pow","Nat.Prime.not_prime_pow'","Nat.Prime.odd_of_ne_two","Nat.Prime.one_le","Nat.Prime.one_lt","Nat.Prime.one_lt'","Nat.Prime.pos","Nat.Prime.pow_eq_iff","Nat.Prime.pred_pos","Nat.Prime.prime","Nat.Prime.two_le","Nat.Primes.coe_nat_inj","Nat.Primes.coe_nat_injective","Nat.add_assoc","Nat.add_comm","Nat.add_coprime_iff_left","Nat.add_coprime_iff_right","Nat.add_zero","Nat.coprime_add_iff_left","Nat.coprime_add_iff_right","Nat.coprime_add_mul_left_left","Nat.coprime_add_mul_left_right","Nat.coprime_add_mul_right_left","Nat.coprime_add_mul_right_right","Nat.coprime_add_self_left","Nat.coprime_add_self_right","Nat.coprime_comm","Nat.coprime_div_gcd_div_gcd","Nat.coprime_iff_gcd_eq_one","Nat.coprime_iff_isRelPrime","Nat.coprime_mul_iff_left","Nat.coprime_mul_iff_right","Nat.coprime_mul_left_add_left","Nat.coprime_mul_left_add_right","Nat.coprime_mul_right_add_left","Nat.coprime_mul_right_add_right","Nat.coprime_of_dvd","Nat.coprime_of_dvd'","Nat.coprime_of_lt_minFac","Nat.coprime_of_lt_prime","Nat.coprime_one_left","Nat.coprime_one_left_eq_true","Nat.coprime_one_left_iff","Nat.coprime_one_right","Nat.coprime_one_right_eq_true","Nat.coprime_one_right_iff","Nat.coprime_or_dvd_of_prime","Nat.coprime_pow_left_iff","Nat.coprime_pow_primes","Nat.coprime_pow_right_iff","Nat.coprime_primes","Nat.coprime_self","Nat.coprime_self_add_left","Nat.coprime_self_add_right","Nat.coprime_self_sub_left","Nat.coprime_self_sub_right","Nat.coprime_sub_self_left","Nat.coprime_sub_self_right","Nat.coprime_two_left","Nat.coprime_two_right","Nat.coprime_zero_left","Nat.coprime_zero_right","Nat.decidablePrime_csimp","Nat.div_gcd_pos_of_pos_left","Nat.div_gcd_pos_of_pos_right","Nat.dvdProdDvdOfDvdProd.proof_1","Nat.dvdProdDvdOfDvdProd.proof_2","Nat.dvdProdDvdOfDvdProd.proof_3","Nat.dvdProdDvdOfDvdProd.proof_4","Nat.dvdProdDvdOfDvdProd.proof_5","Nat.dvd_antisymm","Nat.dvd_gcd","Nat.dvd_gcd_iff","Nat.dvd_gcd_mul_gcd_iff_dvd_mul","Nat.dvd_gcd_mul_iff_dvd_mul","Nat.dvd_mul","Nat.dvd_mul_gcd_iff_dvd_mul","Nat.dvd_mul_left","Nat.dvd_mul_right","Nat.dvd_of_forall_prime_mul_dvd","Nat.dvd_prime","Nat.dvd_prime_pow","Nat.dvd_prime_two_le","Nat.dvd_refl","Nat.dvd_trans","Nat.eq_one_iff_not_exists_prime_dvd","Nat.eq_one_of_dvd_coprimes","Nat.eq_or_coprime_of_le_prime","Nat.eq_prime_pow_of_dvd_least_prime_pow","Nat.eq_zero_of_gcd_eq_zero_left","Nat.eq_zero_of_gcd_eq_zero_right","Nat.exists_coprime","Nat.exists_coprime'","Nat.exists_dvd_of_not_prime","Nat.exists_dvd_of_not_prime2","Nat.exists_prime_and_dvd","Nat.fact_prime_three","Nat.fact_prime_two","Nat.factors_lemma","Nat.gcd","Nat.gcd.eq_1","Nat.gcd.eq_def","Nat.gcd.induction","Nat.gcd_add_left_left_of_dvd","Nat.gcd_add_left_right_of_dvd","Nat.gcd_add_mul_left_left","Nat.gcd_add_mul_left_right","Nat.gcd_add_mul_right_left","Nat.gcd_add_mul_right_right","Nat.gcd_add_mul_self","Nat.gcd_add_one","Nat.gcd_add_right_left_of_dvd","Nat.gcd_add_right_right_of_dvd","Nat.gcd_add_self_left","Nat.gcd_add_self_right","Nat.gcd_assoc","Nat.gcd_comm","Nat.gcd_def","Nat.gcd_div","Nat.gcd_div_gcd_div_gcd_of_pos_left","Nat.gcd_div_gcd_div_gcd_of_pos_right","Nat.gcd_dvd","Nat.gcd_dvd_gcd_mul_left","Nat.gcd_dvd_gcd_mul_left_left","Nat.gcd_dvd_gcd_mul_left_right","Nat.gcd_dvd_gcd_mul_right","Nat.gcd_dvd_gcd_mul_right_left","Nat.gcd_dvd_gcd_mul_right_right","Nat.gcd_dvd_gcd_of_dvd_left","Nat.gcd_dvd_gcd_of_dvd_right","Nat.gcd_dvd_left","Nat.gcd_dvd_right","Nat.gcd_eq_iff","Nat.gcd_eq_left","Nat.gcd_eq_left_iff_dvd","Nat.gcd_eq_one_iff","Nat.gcd_eq_one_of_lt_minFac","Nat.gcd_eq_right","Nat.gcd_eq_right_iff_dvd","Nat.gcd_eq_zero_iff","Nat.gcd_gcd_self_left_left","Nat.gcd_gcd_self_left_right","Nat.gcd_gcd_self_right_left","Nat.gcd_gcd_self_right_right","Nat.gcd_greatest","Nat.gcd_le_left","Nat.gcd_le_right","Nat.gcd_left_eq_iff","Nat.gcd_mul_dvd_mul_gcd","Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime","Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul","Nat.gcd_mul_left","Nat.gcd_mul_left_add_left","Nat.gcd_mul_left_add_right","Nat.gcd_mul_left_left","Nat.gcd_mul_left_left_of_gcd_eq_one","Nat.gcd_mul_left_right","Nat.gcd_mul_left_right_of_gcd_eq_one","Nat.gcd_mul_left_sub_left","Nat.gcd_mul_left_sub_right","Nat.gcd_mul_of_coprime_of_dvd","Nat.gcd_mul_right","Nat.gcd_mul_right_add_left","Nat.gcd_mul_right_add_right","Nat.gcd_mul_right_left","Nat.gcd_mul_right_left_of_gcd_eq_one","Nat.gcd_mul_right_right","Nat.gcd_mul_right_right_of_gcd_eq_one","Nat.gcd_mul_right_sub_left","Nat.gcd_mul_right_sub_right","Nat.gcd_ne_zero_left","Nat.gcd_ne_zero_right","Nat.gcd_one_left","Nat.gcd_one_right","Nat.gcd_pos_of_pos_left","Nat.gcd_pos_of_pos_right","Nat.gcd_pow_left_of_gcd_eq_one","Nat.gcd_pow_right_of_gcd_eq_one","Nat.gcd_rec","Nat.gcd_right_eq_iff","Nat.gcd_self","Nat.gcd_self_add_left","Nat.gcd_self_add_right","Nat.gcd_self_sub_left","Nat.gcd_self_sub_right","Nat.gcd_sub_left_left_of_dvd","Nat.gcd_sub_left_right_of_dvd","Nat.gcd_sub_mul_left_left","Nat.gcd_sub_mul_left_right","Nat.gcd_sub_mul_right_left","Nat.gcd_sub_mul_right_right","Nat.gcd_sub_right_left_of_dvd","Nat.gcd_sub_right_right_of_dvd","Nat.gcd_sub_self_left","Nat.gcd_sub_self_right","Nat.gcd_succ","Nat.gcd_zero_left","Nat.gcd_zero_right","Nat.instCommutativeGcd","Nat.instIdempotentOpGcd","Nat.instLawfulIdentityGcdOfNat","Nat.irreducible_iff_nat_prime","Nat.irreducible_iff_prime","Nat.lcm","Nat.lcm_dvd_iff","Nat.lcm_dvd_mul","Nat.lcm_mul_left","Nat.lcm_mul_right","Nat.lcm_pos","Nat.le_minFac","Nat.le_minFac'","Nat.le_of_dvd","Nat.le_refl","Nat.le_trans","Nat.lt_of_le_of_lt","Nat.lt_of_lt_of_le","Nat.minFac.eq_1","Nat.minFacAux.eq_1","Nat.minFacAux.eq_def","Nat.minFacAux_has_prop","Nat.minFac_dvd","Nat.minFac_eq","Nat.minFac_eq_one_iff","Nat.minFac_eq_two_iff","Nat.minFac_has_prop","Nat.minFac_le","Nat.minFac_le_div","Nat.minFac_le_of_dvd","Nat.minFac_lemma","Nat.minFac_one","Nat.minFac_pos","Nat.minFac_prime","Nat.minFac_sq_le_self","Nat.minFac_two","Nat.minFac_zero","Nat.mul_assoc","Nat.mul_comm","Nat.mul_dvd_mul","Nat.mul_one","Nat.mul_zero","Nat.ne_one_iff_exists_prime_dvd","Nat.not_coprime_of_dvd_of_dvd","Nat.not_coprime_zero_zero","Nat.not_prime_iff_exists_dvd_lt","Nat.not_prime_iff_exists_dvd_ne","Nat.not_prime_iff_minFac_lt","Nat.not_prime_mul","Nat.not_prime_mul'","Nat.not_prime_of_dvd_of_lt","Nat.not_prime_of_dvd_of_ne","Nat.not_prime_one","Nat.not_prime_zero","Nat.one_mul","Nat.pow_dvd_pow_iff","Nat.pow_gcd_pow","Nat.pow_gcd_pow_of_gcd_eq_one","Nat.pow_sub_one_gcd_pow_sub_one","Nat.pow_sub_one_mod_pow_sub_one","Nat.prime_def","Nat.prime_def_le_sqrt","Nat.prime_def_lt","Nat.prime_def_lt'","Nat.prime_def_lt''","Nat.prime_def_minFac","Nat.prime_dvd_prime_iff_eq","Nat.prime_eleven","Nat.prime_eq_prime_of_dvd_pow","Nat.prime_five","Nat.prime_iff","Nat.prime_mul_iff","Nat.prime_of_coprime","Nat.prime_one_false","Nat.prime_seven","Nat.prime_three","Nat.prime_two","Nat.prime_zero_false","Nat.succ","Nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul","Nat.succ_pred_prime","Nat.zero","Nat.zero_add","Nat.zero_mul","Or.inl","Or.inr","True.intro","congrArg","dvd_mul_of_dvd_left","dvd_mul_of_dvd_right","dvd_refl","dvd_trans","le_refl","le_trans","lt_trans","rfl","sorry"],"tactics":["rfl","exact","rw","simp","simpa","have"],"term_operators":["+","-","*","/","%","^"],"have":"fresh local equality with term proof","forbidden":["commands","imports","attributes","options","metaprograms","native_decide","arbitrary tactics","raw declarations"],"limits":{"proof_bytes":16384,"tokens":2048,"depth":32,"tactics":64}},"availability_basis":"validated_release_metadata","worker_readiness":"not_probed"}]}