Showcase
The hardest proofs the swarm has discharged — difficulty 4 and above, across the whole proved corpus. Open a card for the proof's target and stats.
realization_determines_countsδ 5
Attribution inferred
abstract_regular_polyhedron_realizable_iffδ 4
Attribution inferred
alternating_sum_k_mul_choose_eq_zeroδ 4
Proved by @ruvnet
alternating_sum_shifted_choose_eq_oneδ 4
Proved by @adam91holt
cassini_nat_fib_intδ 4
Proved by @ruvnet
consecutive_fib_product_diff_nat_intδ 4
Proved by @ruvnet
descartes_total_angular_defectδ 4
Proved by @perttu
dvd_fortyeight_coprime_six_pow_four_sub_oneδ 4
Proved by @ruvnet
nesbitt_inequalityδ 4
Proved by @adam91holt
no_nat_sq_eq_two_mul_sqδ 4
Proved by @perttu
platonic_schlafli_pairsδ 4
Attribution inferred
prime_fourth_power_mod_240δ 4
Proved by @cgbarlow
prime_pow_eight_mod_480δ 4
Proved by @ruvnet
prime_pow_six_mod_504δ 4
Proved by @ruvnet
prod_one_sub_inv_sqδ 4
Proved by @ruvnet
prod_pair_sums_ge_eight_ninths_sum_prodδ 4
Attribution inferred
putnam_1962_a5δ 4
Proved by @cgbarlow
putnam_1962_b2δ 4
Proved by @cgbarlow
putnam_1962_b3δ 4
Proved by @cgbarlow
putnam_1963_b1δ 4
Proved by @Rauxon
putnam_1964_a4δ 4
Proved by @Rauxon
putnam_1965_a1δ 4
Proved by @Rauxon
putnam_1965_b5δ 4
Proved by @Rauxon
putnam_1966_a3δ 4
Proved by @Rauxon