Trust

Axioms come from the Lean kernel (Lean (version 4.27.0, x86_64-w64-windows-gnu, commit db93fe1608548721853390a10cd40580fe7d22ae, Release)): the constants each declaration depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.

Lake environment and dependency-pin digest: c854fa9c26928ec4.

Verification scope: all declaration-bearing files; 71 of 71 eligible files selected, 3323 declarations requested.

Rendering mode: clean content-bound cache results only; 0 selected files had no reusable result and remain UNKNOWN. No Lean process was started for those misses during this static-site build.

Per-file probe bounds: 1800 seconds. A resource stop is UNKNOWN, never a failed proof.

no axioms

203

standard axioms

3044

sorry

72

extra axioms

0

unknown

4

What the badges mean

no axioms

Lean's kernel checked the proof, and it rests on nothing but Lean's rules.

standard axioms

Checked by the kernel, using only propext, Classical.choice or Quot.sound: the three axioms nearly all of mathematics in Lean uses.

extra axioms

Checked by the kernel, but it assumes something the project declared with `axiom`. It is only as true as those assumptions.

depends on sorry

Not proved: somewhere in it, or in something it uses, a proof was left out (`sorry`).

trust unknown

Lean did not check it: Lean was not run, the file did not elaborate, or Lean has no constant by that name.

Trust UNKNOWN declarations (4)

1. MonochromaticQuantumGraph.eqSystem4_d2_nat APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean trust unknown: Lean has no constant by this name
2. MonochromaticQuantumGraph.eqSystem4_d3_nat APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean trust unknown: Lean has no constant by this name
3. MonochromaticQuantumGraph.eqSystem6_d2_nat APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean trust unknown: Lean has no constant by this name
4. A258667_inner_sum APNOutputs/OEIS/oeis_A258667_conjecture_0.lean trust unknown: Lean has no constant by this name

Depend on sorry (72)

1. OpenQuantumProblem35.ame_5_2_exists APNOutputs/AICollaborator/QuantumOptics/35.lean
2. OpenQuantumProblem35.ame_6_2_exists APNOutputs/AICollaborator/QuantumOptics/35.lean
3. OpenQuantumProblem35.ame_4_2_not_exists APNOutputs/AICollaborator/QuantumOptics/35.lean
4. OpenQuantumProblem35.ame_7_2_not_exists APNOutputs/AICollaborator/QuantumOptics/35.lean
5. OpenQuantumProblem35.ame_4_3_exists APNOutputs/AICollaborator/QuantumOptics/35.lean
6. OpenQuantumProblem35.ame_4_6_exists APNOutputs/AICollaborator/QuantumOptics/35.lean
7. OpenQuantumProblem35.ame_7_6_open APNOutputs/AICollaborator/QuantumOptics/35.lean
8. OpenQuantumProblem35.ame_7_10_open APNOutputs/AICollaborator/QuantumOptics/35.lean
9. OpenQuantumProblem35.ame_8_4_open APNOutputs/AICollaborator/QuantumOptics/35.lean
10. OpenQuantumProblem35.ame_8_6_open APNOutputs/AICollaborator/QuantumOptics/35.lean
11. OpenQuantumProblem35.ame_8_10_open APNOutputs/AICollaborator/QuantumOptics/35.lean
12. OpenQuantumProblem35.ame_9_6_open APNOutputs/AICollaborator/QuantumOptics/35.lean
13. OpenQuantumProblem35.ame_9_10_open APNOutputs/AICollaborator/QuantumOptics/35.lean
14. OpenQuantumProblem35.ame_10_6_open APNOutputs/AICollaborator/QuantumOptics/35.lean
15. OpenQuantumProblem35.ame_10_10_open APNOutputs/AICollaborator/QuantumOptics/35.lean
16. OpenQuantumProblem35.ame_11_3_open APNOutputs/AICollaborator/QuantumOptics/35.lean
17. OpenQuantumProblem35.ame_11_4_open APNOutputs/AICollaborator/QuantumOptics/35.lean
18. OpenQuantumProblem35.ame_11_6_open APNOutputs/AICollaborator/QuantumOptics/35.lean
19. OpenQuantumProblem35.ame_11_10_open APNOutputs/AICollaborator/QuantumOptics/35.lean
20. OpenQuantumProblem35.ame_12_5_open APNOutputs/AICollaborator/QuantumOptics/35.lean
21. OpenQuantumProblem35.ame_12_6_open APNOutputs/AICollaborator/QuantumOptics/35.lean
22. OpenQuantumProblem35.ame_12_10_open APNOutputs/AICollaborator/QuantumOptics/35.lean
23. OpenQuantumProblem35.oqp_35 APNOutputs/AICollaborator/QuantumOptics/35.lean
24. MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
25. MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
26. MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
27. MonochromaticQuantumGraph.eqSystem4_no_solution_d4 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
28. MonochromaticQuantumGraph.eqSystem4_no_solution_ge4 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
29. MonochromaticQuantumGraph.eqSystem6_no_solution_d3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
30. MonochromaticQuantumGraph.eqSystem6_no_solution_d4 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
31. MonochromaticQuantumGraph.eqSystem6_no_solution_d5 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
32. MonochromaticQuantumGraph.eqSystem6_no_solution_d6 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
33. MonochromaticQuantumGraph.eqSystem6_no_solution_ge3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
34. MonochromaticQuantumGraph.eqSystem8_no_solution_d3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
35. MonochromaticQuantumGraph.eqSystem8_no_solution_d10 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
36. MonochromaticQuantumGraph.eqSystem10_no_solution_d3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
37. MonochromaticQuantumGraph.eqSystem10_no_solution_d4 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
38. MonochromaticQuantumGraph.eqSystem10_no_solution_d5 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
39. MonochromaticQuantumGraph.eqSystem10_no_solution_d6 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
40. MonochromaticQuantumGraph.eqSystem10_no_solution_d7 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
41. MonochromaticQuantumGraph.eqSystem10_no_solution_d8 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
42. MonochromaticQuantumGraph.eqSystem10_no_solution_d9 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
43. MonochromaticQuantumGraph.eqSystem10_no_solution_d10 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
44. MonochromaticQuantumGraph.eqSystem12_no_solution_d3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
45. MonochromaticQuantumGraph.eqSystem14_no_solution_d3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
46. MonochromaticQuantumGraph.eqSystem16_no_solution_d3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
47. MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3 APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
48. MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
49. MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
50. MonochromaticQuantumGraph.eqSystem6_no_solution_d5_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
51. MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
52. MonochromaticQuantumGraph.eqSystem8_no_solution_d3_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
53. MonochromaticQuantumGraph.eqSystem8_no_solution_d10_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
54. MonochromaticQuantumGraph.eqSystem10_no_solution_d3_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
55. MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_real APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
56. MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
57. MonochromaticQuantumGraph.eqSystem6_no_solution_d3_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
58. MonochromaticQuantumGraph.eqSystem6_no_solution_d5_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
59. MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
60. MonochromaticQuantumGraph.eqSystem8_no_solution_d3_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
61. MonochromaticQuantumGraph.eqSystem8_no_solution_d10_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
62. MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
63. MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
64. MonochromaticQuantumGraph.eqSystem4_no_solution_d4_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
65. MonochromaticQuantumGraph.eqSystem4_no_solution_ge4_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
66. MonochromaticQuantumGraph.eqSystem6_no_solution_d3_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
67. MonochromaticQuantumGraph.eqSystem6_no_solution_d5_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
68. MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
69. MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
70. MonochromaticQuantumGraph.eqSystem8_no_solution_d10_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
71. MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean
72. MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int APNOutputs/AICollaborator/QuantumOptics/MonochromaticQuantumGraph.lean