Trust

Axioms come from the Lean kernel (Lean (version 4.34.0, x86_64-w64-windows-gnu, commit 293d5d0c0c3f3dded4688b3ccd6a33939ac5102b, 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: 217b6ebe49dab5b3.

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

Rendering mode: clean content-bound cache results only; 19 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

518

standard axioms

7893

sorry

5

extra axioms

0

unknown

299

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.

Files outside this Lean pass (19)

• Compfiles/Usa1981P2.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Assets.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Common.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Components/Base.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Components/CompAnchor.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Components/Footer.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Components/Navbar.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Contests/Imo.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Contests/Usamo.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Gen.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Models/Contests.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Models/Problems.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Pages/All.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Pages/ContestPage.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Pages/Index.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• Dashboard/Pages/ProblemPage.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• SSG/Builder.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• SSG/Html.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering
• SSG/Tags.lean: no clean content-bound result in the selected Lean evidence cache; not rerun during cache-only rendering

Trust UNKNOWN declarations (151)

1. Bulgaria1998P1.check9 Compfiles/Bulgaria1998P1.lean trust unknown: Lean has no constant by this name
2. Bulgaria1998P1.toFin9 Compfiles/Bulgaria1998P1.lean trust unknown: Lean has no constant by this name
3. Bulgaria1998P1.of_check9 Compfiles/Bulgaria1998P1.lean trust unknown: Lean has no constant by this name
4. Imo1989P1.row_injOn Compfiles/Imo1989P1.lean trust unknown: Lean has no constant by this name
5. Imo1989P1.row_image_inj Compfiles/Imo1989P1.lean trust unknown: Lean has no constant by this name
6. one_sub_fract_sqrt_two_mul_gt Compfiles/Imo1991P6.lean trust unknown: Lean has no constant by this name
7. abs_fract_sqrt_two_mul_sub_fract_sqrt_two_mul Compfiles/Imo1991P6.lean trust unknown: Lean has no constant by this name
8. solution Compfiles/Imo1991P6.lean trust unknown: Lean has no constant by this name
9. imo1991_p6 Compfiles/Imo1991P6.lean trust unknown: Lean has no constant by this name
10. Imo1992P5.px Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
11. Imo1992P5.py Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
12. Imo1992P5.pz Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
13. Imo1992P5.zslice Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
14. Imo1992P5.card_sum_slices Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
15. Imo1992P5.slice_le_prod Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
16. Imo1992P5.slice_le_sz Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
17. Imo1992P5.px_disjoint Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
18. Imo1992P5.py_disjoint Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
19. Imo1992P5.sum_px_le Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
20. Imo1992P5.sum_py_le Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
21. Imo1992P5.main Compfiles/Imo1992P5.lean trust unknown: Lean has no constant by this name
22. Imo2008P5.fiber_ncard_of_mod_n Compfiles/Imo2008P5.lean trust unknown: Lean has no constant by this name
23. Imo2008P5.ψ Compfiles/Imo2008P5.lean trust unknown: Lean has no constant by this name
24. Imo2008P5.symmDiff_singleton_card_parity Compfiles/Imo2008P5.lean trust unknown: Lean has no constant by this name
25. Imo2008P5.even_subsets_card Compfiles/Imo2008P5.lean trust unknown: Lean has no constant by this name
26. Imo2008P5.claim Compfiles/Imo2008P5.lean trust unknown: Lean has no constant by this name
27. Imo2008P5.lemma1 Compfiles/Imo2008P5.lean trust unknown: Lean has no constant by this name
28. Imo2009P5.pnat_to_nat_prop Compfiles/Imo2009P5.lean trust unknown: Lean has no constant by this name
29. Imo2009P5.pnat_to_nat_prop2 Compfiles/Imo2009P5.lean trust unknown: Lean has no constant by this name
30. Imo2009P5.succ_pnat_add_succ_pnat Compfiles/Imo2009P5.lean trust unknown: Lean has no constant by this name
31. Imo2018P3.NR Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
32. Imo2018P3.TN Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
33. Imo2018P3.NR_val Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
34. Imo2018P3.TN_def Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
35. Imo2018P3.tri Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
36. Imo2018P3.mem_tri Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
37. Imo2018P3.card_tri Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
38. Imo2018P3.min_sum Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
39. Imo2018P3.min_sum_eq Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
40. Imo2018P3.two_mul_sum Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
41. Imo2018P3.min_sum_ge Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
42. Imo2018P3.bijection Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
43. Imo2018P3.winner Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
44. Imo2018P3.loser Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
45. Imo2018P3.winner_row Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
46. Imo2018P3.loser_row Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
47. Imo2018P3.winner_col Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
48. Imo2018P3.loser_col Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
49. Imo2018P3.winner_val Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
50. Imo2018P3.left_child_mem Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
51. Imo2018P3.right_child_mem Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
52. Imo2018P3.winner_mem Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
53. Imo2018P3.loser_mem Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
54. Imo2018P3.chain Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
55. Imo2018P3.chain_zero Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
56. Imo2018P3.chain_succ Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
57. Imo2018P3.chain_row Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
58. Imo2018P3.chain_mem Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
59. Imo2018P3.chain_step_val Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
60. Imo2018P3.chain_sum Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
61. Imo2018P3.losers Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
62. Imo2018P3.smallCells Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
63. Imo2018P3.loser_chain_row Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
64. Imo2018P3.losers_inj Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
65. Imo2018P3.chain_zero_not_losers Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
66. Imo2018P3.losers_card Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
67. Imo2018P3.smallCells_card Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
68. Imo2018P3.smallCells_subset Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
69. Imo2018P3.smallCells_sum Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
70. Imo2018P3.smallCells_injOn Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
71. Imo2018P3.chain_bottom Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
72. Imo2018P3.smallCells_image Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
73. Imo2018P3.not_small Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
74. Imo2018P3.chain_col_le_succ Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
75. Imo2018P3.chain_col_succ_le Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
76. Imo2018P3.chain_col_mono Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
77. Imo2018P3.chain_col_le_add Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
78. Imo2018P3.smallCells_col Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
79. Imo2018P3.notMem_small_left Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
80. Imo2018P3.notMem_small_right Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
81. Imo2018P3.walk Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
82. Imo2018P3.walk_zero Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
83. Imo2018P3.walk_succ Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
84. Imo2018P3.walk_row Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
85. Imo2018P3.walk_sum Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
86. Imo2018P3.inSub Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
87. Imo2018P3.inSub_left Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
88. Imo2018P3.inSub_right Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
89. Imo2018P3.inSub_winner Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
90. Imo2018P3.inSub_loser Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
91. Imo2018P3.walk_inSub Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
92. Imo2018P3.corner_contra Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
93. Imo2018P3.not_exists_desired Compfiles/Imo2018P3.lean trust unknown: Lean has no constant by this name
94. Imo2025P6.incSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
95. Imo2025P6.decSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
96. Imo2025P6.one_mem_incSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
97. Imo2025P6.one_mem_decSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
98. Imo2025P6.incSequencesTo_nonempty Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
99. Imo2025P6.decSequencesTo_nonempty Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
100. Imo2025P6.maxIncSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
101. Imo2025P6.maxDecSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
102. Imo2025P6.one_le_maxIncSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
103. Imo2025P6.one_le_maxDecSequencesTo Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
104. Imo2025P6.maxIncSequencesTo_mem Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
105. Imo2025P6.maxDecSequencesTo_mem Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
106. Imo2025P6.maxIncSequencesTo_lt Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
107. Imo2025P6.maxDecSequencesTo_gt Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
108. Imo2025P6.paired Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
109. Imo2025P6.paired_injective Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
110. Imo2025P6.erdos_szekeres Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
111. Imo2025P6.Label.source_ne_of_ne Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
112. Imo2025P6.fin_ne_sub_one Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
113. Imo2025P6.fin_ne_add_one Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
114. Imo2025P6.label_pos_W_absurd Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
115. Imo2025P6.label_pos_N_absurd Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
116. Imo2025P6.label_pos_E_absurd Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
117. Imo2025P6.label_pos_S_absurd Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
118. Imo2025P6.DisjointSetup.u_not_between_uk_uk1 Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
119. Imo2025P6.DisjointSetup.v_not_between_vl_vl1 Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
120. Imo2025P6.DisjointSetup.covers_X_other Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
121. Imo2025P6.exists_maximal_subset Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
122. Imo2025P6.sqrt_kk Compfiles/Imo2025P6.lean trust unknown: Lean has no constant by this name
123. Imo2026P3.CodexClosePoints.zip_tail_rel Compfiles/Imo2026P3.lean trust unknown: Lean has no constant by this name
124. Imo2026P3.CodexClosePoints.zip_tail_sum Compfiles/Imo2026P3.lean trust unknown: Lean has no constant by this name
125. Usa1993P3.dyadicBracket Compfiles/Usa1993P3.lean trust unknown: Lean has no constant by this name
126. Usa2008P6.ite_eq_one_add Compfiles/Usa2008P6.lean trust unknown: Lean has no constant by this name
127. Usa2008P6.mul_self_eq Compfiles/Usa2008P6.lean trust unknown: Lean has no constant by this name
128. Usa2013P3.Count.period_shift Compfiles/Usa2013P3.lean trust unknown: Lean has no constant by this name
129. Usa2013P3.Count.card_filter_range_four_mul Compfiles/Usa2013P3.lean trust unknown: Lean has no constant by this name
130. Usamo2020P3.setA' Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
131. Usamo2020P3.setB' Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
132. Usamo2020P3.setC' Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
133. Usamo2020P3.isSquare_mul_iff_same Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
134. Usamo2020P3.setC_eq_union Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
135. Usamo2020P3.disjoint_AB Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
136. Usamo2020P3.p_two_ne_zero Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
137. Usamo2020P3.p_two_ne_four Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
138. Usamo2020P3.two_mem_setC Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
139. Usamo2020P3.map_mem_setB Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
140. Usamo2020P3.fiber_prod Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
141. Usamo2020P3.prod_C_erase_eq_prod_B Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
142. Usamo2020P3.prod_B_ne_zero Compfiles/Usa2020P3.lean trust unknown: Lean has no constant by this name
143. Usa2020P4.goodSets Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
144. Usa2020P4.goodPairs Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
145. Usa2020P4.det_swap Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
146. Usa2020P4.eq_zero_of_eq_add_mul Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
147. Usa2020P4.eq_of_det_eq_of_le Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
148. Usa2020P4.gcd_dvd_det Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
149. Usa2020P4.card_partners_le_two Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
150. Usa2020P4.card_goodSets_le Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name
151. Usa2020P4.card_goodPairs_eq Compfiles/Usa2020P4.lean trust unknown: Lean has no constant by this name

Depend on sorry (5)

1. Bulgaria1998P2.bulgaria1998_p2 Compfiles/Bulgaria1998P2.lean
2. Imo2021P3.imo2021_p3 Compfiles/Imo2021P3.lean
3. Imo2023P6.imo2023_p6 Compfiles/Imo2023P6.lean
4. Imo2025P2.imo2025_p2 Compfiles/Imo2025P2.lean
5. Usa1988P4.usa1988_p4 Compfiles/Usa1988P4.lean