Trust

Axioms come from the Lean kernel (Lean (version 4.30.0, x86_64-w64-windows-gnu, commit d024af099ca4bf2c86f649261ebf59565dc8c622, 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: a6dfb4491d992b0d.

Verification scope: all declaration-bearing files; 63 of 63 eligible files selected, 599 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: 300 seconds. A resource stop is UNKNOWN, never a failed proof.

no axioms
238
standard axioms
250
sorry
108
extra axioms
0
unknown
3

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 (3)

  1. C05S03._root_.Nat.Prime.eq_of_dvd_of_prime MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean trust unknown: Lean has no constant by this name
  2. C05S03._root_.Nat.Prime.eq_of_dvd_of_prime MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean trust unknown: Lean has no constant by this name
  3. aux MIL/C07_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean trust unknown: Lean has no constant by this name

Depend on sorry (108)

  1. hard MIL/C01_Introduction/S02_Overview.lean
  2. MyRing.add_neg_cancel_right MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  3. MyRing.add_left_cancel MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  4. MyRing.add_right_cancel MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  5. MyRing.mul_zero MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  6. MyRing.zero_mul MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  7. MyRing.neg_eq_of_add_eq_zero MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  8. MyRing.eq_neg_of_add_eq_zero MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  9. MyRing.neg_zero MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  10. MyRing.neg_neg MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  11. MyRing.self_sub MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  12. MyRing.two_mul MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  13. MyGroup.mul_inv_cancel MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  14. MyGroup.mul_one MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  15. MyGroup.mul_inv_rev MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
  16. C02S04.aux MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean
  17. absorb1 MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
  18. absorb2 MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
  19. C03S01.my_lemma MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
  20. C03S01.my_lemma2 MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
  21. C03S01.my_lemma3 MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
  22. C03S01.my_lemma4 MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
  23. C03S01.Subset.trans MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
  24. C03S04.aux MIL/C03_Logic/S04_Conjunction_and_Iff.lean
  25. C03S05.MyAbs.le_abs_self MIL/C03_Logic/S05_Disjunction.lean
  26. C03S05.MyAbs.neg_le_abs MIL/C03_Logic/S05_Disjunction.lean
  27. C03S05.MyAbs.abs_add_le MIL/C03_Logic/S05_Disjunction.lean
  28. C03S05.MyAbs.lt_abs MIL/C03_Logic/S05_Disjunction.lean
  29. C03S05.MyAbs.abs_lt MIL/C03_Logic/S05_Disjunction.lean
  30. C03S06.convergesTo_add MIL/C03_Logic/S06_Sequences_and_Convergence.lean
  31. C03S06.convergesTo_mul_const MIL/C03_Logic/S06_Sequences_and_Convergence.lean
  32. C03S06.exists_abs_le_of_convergesTo MIL/C03_Logic/S06_Sequences_and_Convergence.lean
  33. C03S06.aux MIL/C03_Logic/S06_Sequences_and_Convergence.lean
  34. C03S06.convergesTo_mul MIL/C03_Logic/S06_Sequences_and_Convergence.lean
  35. C03S06.convergesTo_unique MIL/C03_Logic/S06_Sequences_and_Convergence.lean
  36. Cantor MIL/C04_Sets_and_Functions/S02_Functions.lean
  37. sb_right_inv MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
  38. sb_injective MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
  39. sb_surjective MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
  40. schroeder_bernstein MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
  41. pow_two_le_fac MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  42. sum_sqr MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  43. MyNat.add_assoc MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  44. MyNat.mul_add MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  45. MyNat.zero_mul MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  46. MyNat.succ_mul MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  47. MyNat.mul_comm MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
  48. C05S03.primes_infinite MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
  49. C05S03.mem_of_dvd_prod_primes MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
  50. C05S03.primes_infinite' MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
  51. C05S03.aux MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
  52. C05S03.exists_prime_factor_mod_4_eq_3 MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
  53. C05S03.primes_mod_4_eq_3_infinite MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean
  54. MyListSpace3.reverse MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  55. MyListSpace3.reverse_append MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  56. MyListSpace3.reverse_reverse MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  57. BinTree.depth_le_size MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  58. BinTree.flip MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  59. BinTree.size_flip MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  60. PropForm.subst_eq_of_not_mem_vars MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  61. PropForm.subst_eval_eq MIL/C06_Discrete_Mathematics/S03_Inductive_Structures.lean
  62. C06S01.Point.add_assoc MIL/C07_Structures/S01_Structures.lean
  63. C06S01.Point.smul MIL/C07_Structures/S01_Structures.lean
  64. C06S01.Point.smul_distrib MIL/C07_Structures/S01_Structures.lean
  65. C06S01.StandardTwoSimplex.weightedAverage MIL/C07_Structures/S01_Structures.lean
  66. C06S02.Point.neg MIL/C07_Structures/S02_Algebraic_Structures.lean
  67. C06S02.Point.zero MIL/C07_Structures/S02_Algebraic_Structures.lean
  68. C06S02.Point.addGroupPoint MIL/C07_Structures/S02_Algebraic_Structures.lean
  69. sq_add_sq_eq_zero MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  70. GaussInt.norm_nonneg MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  71. GaussInt.norm_eq_zero MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  72. GaussInt.norm_pos MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  73. GaussInt.norm_mul MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  74. GaussInt.norm_mod_lt MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  75. GaussInt.coe_natAbs_norm MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  76. GaussInt.natAbs_norm_mod_lt MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  77. GaussInt.not_norm_mul_left_lt_norm MIL/C07_Structures/S03_Building_the_Gaussian_Integers.lean
  78. inv_eq_of_dia MIL/C08_Hierarchies/S01_Basics.lean
  79. dia_inv MIL/C08_Hierarchies/S01_Basics.lean
  80. inv_eq_of_mul MIL/C08_Hierarchies/S01_Basics.lean
  81. Group₃.mul_inv MIL/C08_Hierarchies/S01_Basics.lean
  82. mul_left_cancel₃ MIL/C08_Hierarchies/S01_Basics.lean
  83. mul_right_cancel₃ MIL/C08_Hierarchies/S01_Basics.lean
  84. Module₁ MIL/C08_Hierarchies/S01_Basics.lean
  85. selfModule MIL/C08_Hierarchies/S01_Basics.lean
  86. abGrpModule MIL/C08_Hierarchies/S01_Basics.lean
  87. Submonoid.Setoid MIL/C08_Hierarchies/S03_Subobjects.lean
  88. QuotientMonoid.mk MIL/C08_Hierarchies/S03_Subobjects.lean
  89. abGrpModule MIL/C08_Hierarchies/solutions/Solutions_S01_Basics.lean
  90. conjugate MIL/C09_Groups_and_Rings/S01_Groups.lean
  91. eq_bot_iff_card MIL/C09_Groups_and_Rings/S01_Groups.lean
  92. inf_bot_of_coprime MIL/C09_Groups_and_Rings/S01_Groups.lean
  93. conjugate_one MIL/C09_Groups_and_Rings/S01_Groups.lean
  94. aux_card_eq MIL/C09_Groups_and_Rings/S01_Groups.lean
  95. iso₁ MIL/C09_Groups_and_Rings/S01_Groups.lean
  96. iso₂ MIL/C09_Groups_and_Rings/S01_Groups.lean
  97. finalIso MIL/C09_Groups_and_Rings/S01_Groups.lean
  98. chineseMap MIL/C09_Groups_and_Rings/S02_Rings.lean
  99. chineseMap_mk MIL/C09_Groups_and_Rings/S02_Rings.lean
  100. chineseMap_mk' MIL/C09_Groups_and_Rings/S02_Rings.lean
  101. chineseMap_inj MIL/C09_Groups_and_Rings/S02_Rings.lean
  102. isCoprime_Inf MIL/C09_Groups_and_Rings/S02_Rings.lean
  103. chineseMap_surj MIL/C09_Groups_and_Rings/S02_Rings.lean
  104. chineseIso MIL/C09_Groups_and_Rings/S02_Rings.lean
  105. preimage MIL/C10_Linear_Algebra/S02_Subspaces.lean
  106. principal MIL/C11_Topology/S01_Filters.lean
  107. cauchySeq_of_le_geometric_two' MIL/C11_Topology/S02_Metric_Spaces.lean
  108. aux MIL/C11_Topology/S03_Topological_Spaces.lean