Unsorry

Proof graph · 762 goals
324 open 3 blocked 9 translated 288 proved 138 archived
Diagram 
flowchart LR
  classDef proved fill:#c6f6d5,stroke:#4a5568,color:#1a202c;
  classDef open fill:#e2e8f0,stroke:#4a5568,color:#1a202c;
  classDef blocked fill:#feebc8,stroke:#4a5568,color:#1a202c;
  classDef flagged fill:#fed7d7,stroke:#4a5568,color:#1a202c;
  classDef translated fill:#bee3f8,stroke:#4a5568,color:#1a202c;
  classDef unknown fill:#edf2f7,stroke:#4a5568,color:#1a202c;
  g_am_gm_three_cube["am-gm-three-cube"]
  class g_am_gm_three_cube open;
  click g_am_gm_three_cube call showDetail("am-gm-three-cube")
  g_am_gm_three_cube_s1["am-gm-three-cube-s1"]
  class g_am_gm_three_cube_s1 proved;
  click g_am_gm_three_cube_s1 call showDetail("am-gm-three-cube-s1")
  g_am_gm_three_cube_s2["am-gm-three-cube-s2"]
  class g_am_gm_three_cube_s2 proved;
  click g_am_gm_three_cube_s2 call showDetail("am-gm-three-cube-s2")
  g_am_gm_three_cube_s2_s1["am-gm-three-cube-s2-s1"]
  class g_am_gm_three_cube_s2_s1 proved;
  click g_am_gm_three_cube_s2_s1 call showDetail("am-gm-three-cube-s2-s1")
  g_am_gm_three_cube_s2_s2["am-gm-three-cube-s2-s2"]
  class g_am_gm_three_cube_s2_s2 proved;
  click g_am_gm_three_cube_s2_s2 call showDetail("am-gm-three-cube-s2-s2")
  g_am_gm_three_cube_s2_s2_s1["am-gm-three-cube-s2-s2-s1"]
  class g_am_gm_three_cube_s2_s2_s1 proved;
  click g_am_gm_three_cube_s2_s2_s1 call showDetail("am-gm-three-cube-s2-s2-s1")
  g_am_gm_three_cube_s2_s2_s2["am-gm-three-cube-s2-s2-s2"]
  class g_am_gm_three_cube_s2_s2_s2 proved;
  click g_am_gm_three_cube_s2_s2_s2 call showDetail("am-gm-three-cube-s2-s2-s2")
  g_am_hm_two_var["am-hm-two-var"]
  class g_am_hm_two_var open;
  click g_am_hm_two_var call showDetail("am-hm-two-var")
  g_am_hm_two_var_s1["am-hm-two-var-s1"]
  class g_am_hm_two_var_s1 proved;
  click g_am_hm_two_var_s1 call showDetail("am-hm-two-var-s1")
  g_am_hm_two_var_s2["am-hm-two-var-s2"]
  class g_am_hm_two_var_s2 proved;
  click g_am_hm_two_var_s2 call showDetail("am-hm-two-var-s2")
  g_am_hm_two_var_s3["am-hm-two-var-s3"]
  class g_am_hm_two_var_s3 proved;
  click g_am_hm_two_var_s3 call showDetail("am-hm-two-var-s3")
  g_cube_sum_ge_three_prod["cube-sum-ge-three-prod"]
  class g_cube_sum_ge_three_prod proved;
  click g_cube_sum_ge_three_prod call showDetail("cube-sum-ge-three-prod")
  g_cube_sum_ge_three_prod_s1["cube-sum-ge-three-prod-s1"]
  class g_cube_sum_ge_three_prod_s1 proved;
  click g_cube_sum_ge_three_prod_s1 call showDetail("cube-sum-ge-three-prod-s1")
  g_cube_sum_ge_three_prod_s2["cube-sum-ge-three-prod-s2"]
  class g_cube_sum_ge_three_prod_s2 proved;
  click g_cube_sum_ge_three_prod_s2 call showDetail("cube-sum-ge-three-prod-s2")
  g_cube_sum_ge_three_prod_s3["cube-sum-ge-three-prod-s3"]
  class g_cube_sum_ge_three_prod_s3 proved;
  click g_cube_sum_ge_three_prod_s3 call showDetail("cube-sum-ge-three-prod-s3")
  g_discriminant_nonneg["discriminant-nonneg"]
  class g_discriminant_nonneg proved;
  click g_discriminant_nonneg call showDetail("discriminant-nonneg")
  g_discriminant_nonneg_s1["discriminant-nonneg-s1"]
  class g_discriminant_nonneg_s1 proved;
  click g_discriminant_nonneg_s1 call showDetail("discriminant-nonneg-s1")
  g_discriminant_nonneg_s2["discriminant-nonneg-s2"]
  class g_discriminant_nonneg_s2 proved;
  click g_discriminant_nonneg_s2 call showDetail("discriminant-nonneg-s2")
  g_discriminant_nonneg_s3["discriminant-nonneg-s3"]
  class g_discriminant_nonneg_s3 proved;
  click g_discriminant_nonneg_s3 call showDetail("discriminant-nonneg-s3")
  g_dvd_210_pow_fifteen_sub_pow_three["dvd-210-pow-fifteen-sub-pow-three"]
  class g_dvd_210_pow_fifteen_sub_pow_three open;
  click g_dvd_210_pow_fifteen_sub_pow_three call showDetail("dvd-210-pow-fifteen-sub-pow-three")
  g_dvd_210_pow_fifteen_sub_pow_three_s1["dvd-210-pow-fifteen-sub-pow-three-s1"]
  class g_dvd_210_pow_fifteen_sub_pow_three_s1 proved;
  click g_dvd_210_pow_fifteen_sub_pow_three_s1 call showDetail("dvd-210-pow-fifteen-sub-pow-three-s1")
  g_dvd_210_pow_fifteen_sub_pow_three_s2["dvd-210-pow-fifteen-sub-pow-three-s2"]
  class g_dvd_210_pow_fifteen_sub_pow_three_s2 proved;
  click g_dvd_210_pow_fifteen_sub_pow_three_s2 call showDetail("dvd-210-pow-fifteen-sub-pow-three-s2")
  g_dvd_210_pow_fifteen_sub_pow_three_s3["dvd-210-pow-fifteen-sub-pow-three-s3"]
  class g_dvd_210_pow_fifteen_sub_pow_three_s3 proved;
  click g_dvd_210_pow_fifteen_sub_pow_three_s3 call showDetail("dvd-210-pow-fifteen-sub-pow-three-s3")
  g_dvd_210_pow_fifteen_sub_pow_three_s4["dvd-210-pow-fifteen-sub-pow-three-s4"]
  class g_dvd_210_pow_fifteen_sub_pow_three_s4 proved;
  click g_dvd_210_pow_fifteen_sub_pow_three_s4 call showDetail("dvd-210-pow-fifteen-sub-pow-three-s4")
  g_four_var_qm_am["four-var-qm-am"]
  class g_four_var_qm_am proved;
  click g_four_var_qm_am call showDetail("four-var-qm-am")
  g_four_var_qm_am_s1["four-var-qm-am-s1"]
  class g_four_var_qm_am_s1 proved;
  click g_four_var_qm_am_s1 call showDetail("four-var-qm-am-s1")
  g_four_var_qm_am_s2["four-var-qm-am-s2"]
  class g_four_var_qm_am_s2 proved;
  click g_four_var_qm_am_s2 call showDetail("four-var-qm-am-s2")
  g_four_var_qm_am_s3["four-var-qm-am-s3"]
  class g_four_var_qm_am_s3 proved;
  click g_four_var_qm_am_s3 call showDetail("four-var-qm-am-s3")
  g_nat_sq_lt_two_pow["nat-sq-lt-two-pow"]
  class g_nat_sq_lt_two_pow proved;
  click g_nat_sq_lt_two_pow call showDetail("nat-sq-lt-two-pow")
  g_nat_sq_lt_two_pow_s1["nat-sq-lt-two-pow-s1"]
  class g_nat_sq_lt_two_pow_s1 proved;
  click g_nat_sq_lt_two_pow_s1 call showDetail("nat-sq-lt-two-pow-s1")
  g_nat_sq_lt_two_pow_s2["nat-sq-lt-two-pow-s2"]
  class g_nat_sq_lt_two_pow_s2 open;
  click g_nat_sq_lt_two_pow_s2 call showDetail("nat-sq-lt-two-pow-s2")
  g_nat_sq_lt_two_pow_s2_s1["nat-sq-lt-two-pow-s2-s1"]
  class g_nat_sq_lt_two_pow_s2_s1 proved;
  click g_nat_sq_lt_two_pow_s2_s1 call showDetail("nat-sq-lt-two-pow-s2-s1")
  g_nat_sq_lt_two_pow_s2_s2["nat-sq-lt-two-pow-s2-s2"]
  class g_nat_sq_lt_two_pow_s2_s2 proved;
  click g_nat_sq_lt_two_pow_s2_s2 call showDetail("nat-sq-lt-two-pow-s2-s2")
  g_nat_sq_lt_two_pow_s2_s3["nat-sq-lt-two-pow-s2-s3"]
  class g_nat_sq_lt_two_pow_s2_s3 proved;
  click g_nat_sq_lt_two_pow_s2_s3 call showDetail("nat-sq-lt-two-pow-s2-s3")
  g_nesbitt_inequality["nesbitt-inequality"]
  class g_nesbitt_inequality blocked;
  click g_nesbitt_inequality call showDetail("nesbitt-inequality")
  g_nesbitt_inequality_s1["nesbitt-inequality-s1"]
  class g_nesbitt_inequality_s1 open;
  click g_nesbitt_inequality_s1 call showDetail("nesbitt-inequality-s1")
  g_nesbitt_inequality_s2["nesbitt-inequality-s2"]
  class g_nesbitt_inequality_s2 proved;
  click g_nesbitt_inequality_s2 call showDetail("nesbitt-inequality-s2")
  g_nesbitt_inequality_s3["nesbitt-inequality-s3"]
  class g_nesbitt_inequality_s3 proved;
  click g_nesbitt_inequality_s3 call showDetail("nesbitt-inequality-s3")
  g_nesbitt_inequality_s4["nesbitt-inequality-s4"]
  class g_nesbitt_inequality_s4 proved;
  click g_nesbitt_inequality_s4 call showDetail("nesbitt-inequality-s4")
  g_no_nat_sq_eq_two_mul_sq["no-nat-sq-eq-two-mul-sq"]
  class g_no_nat_sq_eq_two_mul_sq proved;
  click g_no_nat_sq_eq_two_mul_sq call showDetail("no-nat-sq-eq-two-mul-sq")
  g_no_nat_sq_eq_two_mul_sq_s1["no-nat-sq-eq-two-mul-sq-s1"]
  class g_no_nat_sq_eq_two_mul_sq_s1 proved;
  click g_no_nat_sq_eq_two_mul_sq_s1 call showDetail("no-nat-sq-eq-two-mul-sq-s1")
  g_no_nat_sq_eq_two_mul_sq_s2["no-nat-sq-eq-two-mul-sq-s2"]
  class g_no_nat_sq_eq_two_mul_sq_s2 proved;
  click g_no_nat_sq_eq_two_mul_sq_s2 call showDetail("no-nat-sq-eq-two-mul-sq-s2")
  g_no_nat_sq_eq_two_mul_sq_s3["no-nat-sq-eq-two-mul-sq-s3"]
  class g_no_nat_sq_eq_two_mul_sq_s3 proved;
  click g_no_nat_sq_eq_two_mul_sq_s3 call showDetail("no-nat-sq-eq-two-mul-sq-s3")
  g_no_nat_sq_eq_two_mul_sq_s4["no-nat-sq-eq-two-mul-sq-s4"]
  class g_no_nat_sq_eq_two_mul_sq_s4 proved;
  click g_no_nat_sq_eq_two_mul_sq_s4 call showDetail("no-nat-sq-eq-two-mul-sq-s4")
  g_six_dvd_pow_three_add_five_mul["six-dvd-pow-three-add-five-mul"]
  class g_six_dvd_pow_three_add_five_mul open;
  click g_six_dvd_pow_three_add_five_mul call showDetail("six-dvd-pow-three-add-five-mul")
  g_six_dvd_pow_three_add_five_mul_s1["six-dvd-pow-three-add-five-mul-s1"]
  class g_six_dvd_pow_three_add_five_mul_s1 proved;
  click g_six_dvd_pow_three_add_five_mul_s1 call showDetail("six-dvd-pow-three-add-five-mul-s1")
  g_six_dvd_pow_three_add_five_mul_s2["six-dvd-pow-three-add-five-mul-s2"]
  class g_six_dvd_pow_three_add_five_mul_s2 proved;
  click g_six_dvd_pow_three_add_five_mul_s2 call showDetail("six-dvd-pow-three-add-five-mul-s2")
  g_sq_add_sq_eq_three_mul_sq["sq-add-sq-eq-three-mul-sq"]
  class g_sq_add_sq_eq_three_mul_sq blocked;
  click g_sq_add_sq_eq_three_mul_sq call showDetail("sq-add-sq-eq-three-mul-sq")
  g_sq_add_sq_eq_three_mul_sq_s1["sq-add-sq-eq-three-mul-sq-s1"]
  class g_sq_add_sq_eq_three_mul_sq_s1 proved;
  click g_sq_add_sq_eq_three_mul_sq_s1 call showDetail("sq-add-sq-eq-three-mul-sq-s1")
  g_sq_add_sq_eq_three_mul_sq_s2["sq-add-sq-eq-three-mul-sq-s2"]
  class g_sq_add_sq_eq_three_mul_sq_s2 proved;
  click g_sq_add_sq_eq_three_mul_sq_s2 call showDetail("sq-add-sq-eq-three-mul-sq-s2")
  g_sq_add_sq_eq_three_mul_sq_s3["sq-add-sq-eq-three-mul-sq-s3"]
  class g_sq_add_sq_eq_three_mul_sq_s3 proved;
  click g_sq_add_sq_eq_three_mul_sq_s3 call showDetail("sq-add-sq-eq-three-mul-sq-s3")
  g_sq_add_sq_eq_three_mul_sq_s4["sq-add-sq-eq-three-mul-sq-s4"]
  class g_sq_add_sq_eq_three_mul_sq_s4 open;
  click g_sq_add_sq_eq_three_mul_sq_s4 call showDetail("sq-add-sq-eq-three-mul-sq-s4")
  g_sum_icc_choose_hockey_stick["sum-icc-choose-hockey-stick"]
  class g_sum_icc_choose_hockey_stick blocked;
  click g_sum_icc_choose_hockey_stick call showDetail("sum-icc-choose-hockey-stick")
  g_sum_icc_choose_hockey_stick_s1["sum-icc-choose-hockey-stick-s1"]
  class g_sum_icc_choose_hockey_stick_s1 open;
  click g_sum_icc_choose_hockey_stick_s1 call showDetail("sum-icc-choose-hockey-stick-s1")
  g_sum_icc_choose_hockey_stick_s2["sum-icc-choose-hockey-stick-s2"]
  class g_sum_icc_choose_hockey_stick_s2 open;
  click g_sum_icc_choose_hockey_stick_s2 call showDetail("sum-icc-choose-hockey-stick-s2")
  g_sum_icc_choose_hockey_stick_s3["sum-icc-choose-hockey-stick-s3"]
  class g_sum_icc_choose_hockey_stick_s3 open;
  click g_sum_icc_choose_hockey_stick_s3 call showDetail("sum-icc-choose-hockey-stick-s3")
  g_am_gm_three_cube --> g_am_gm_three_cube_s1
  g_am_gm_three_cube --> g_am_gm_three_cube_s2
  g_am_gm_three_cube_s2 --> g_am_gm_three_cube_s2_s1
  g_am_gm_three_cube_s2 --> g_am_gm_three_cube_s2_s2
  g_am_gm_three_cube_s2_s2 --> g_am_gm_three_cube_s2_s2_s1
  g_am_gm_three_cube_s2_s2 --> g_am_gm_three_cube_s2_s2_s2
  g_am_hm_two_var --> g_am_hm_two_var_s1
  g_am_hm_two_var --> g_am_hm_two_var_s2
  g_am_hm_two_var --> g_am_hm_two_var_s3
  g_cube_sum_ge_three_prod --> g_cube_sum_ge_three_prod_s1
  g_cube_sum_ge_three_prod --> g_cube_sum_ge_three_prod_s2
  g_cube_sum_ge_three_prod --> g_cube_sum_ge_three_prod_s3
  g_discriminant_nonneg --> g_discriminant_nonneg_s1
  g_discriminant_nonneg --> g_discriminant_nonneg_s2
  g_discriminant_nonneg --> g_discriminant_nonneg_s3
  g_dvd_210_pow_fifteen_sub_pow_three --> g_dvd_210_pow_fifteen_sub_pow_three_s1
  g_dvd_210_pow_fifteen_sub_pow_three --> g_dvd_210_pow_fifteen_sub_pow_three_s2
  g_dvd_210_pow_fifteen_sub_pow_three --> g_dvd_210_pow_fifteen_sub_pow_three_s3
  g_dvd_210_pow_fifteen_sub_pow_three --> g_dvd_210_pow_fifteen_sub_pow_three_s4
  g_four_var_qm_am --> g_four_var_qm_am_s1
  g_four_var_qm_am --> g_four_var_qm_am_s2
  g_four_var_qm_am --> g_four_var_qm_am_s3
  g_nat_sq_lt_two_pow --> g_nat_sq_lt_two_pow_s1
  g_nat_sq_lt_two_pow --> g_nat_sq_lt_two_pow_s2
  g_nat_sq_lt_two_pow_s2 --> g_nat_sq_lt_two_pow_s2_s1
  g_nat_sq_lt_two_pow_s2 --> g_nat_sq_lt_two_pow_s2_s2
  g_nat_sq_lt_two_pow_s2 --> g_nat_sq_lt_two_pow_s2_s3
  g_nesbitt_inequality --> g_nesbitt_inequality_s1
  g_nesbitt_inequality --> g_nesbitt_inequality_s2
  g_nesbitt_inequality --> g_nesbitt_inequality_s3
  g_nesbitt_inequality --> g_nesbitt_inequality_s4
  g_no_nat_sq_eq_two_mul_sq --> g_no_nat_sq_eq_two_mul_sq_s1
  g_no_nat_sq_eq_two_mul_sq --> g_no_nat_sq_eq_two_mul_sq_s2
  g_no_nat_sq_eq_two_mul_sq --> g_no_nat_sq_eq_two_mul_sq_s3
  g_no_nat_sq_eq_two_mul_sq --> g_no_nat_sq_eq_two_mul_sq_s4
  g_six_dvd_pow_three_add_five_mul --> g_six_dvd_pow_three_add_five_mul_s1
  g_six_dvd_pow_three_add_five_mul --> g_six_dvd_pow_three_add_five_mul_s2
  g_sq_add_sq_eq_three_mul_sq --> g_sq_add_sq_eq_three_mul_sq_s1
  g_sq_add_sq_eq_three_mul_sq --> g_sq_add_sq_eq_three_mul_sq_s2
  g_sq_add_sq_eq_three_mul_sq --> g_sq_add_sq_eq_three_mul_sq_s3
  g_sq_add_sq_eq_three_mul_sq --> g_sq_add_sq_eq_three_mul_sq_s4
  g_sum_icc_choose_hockey_stick --> g_sum_icc_choose_hockey_stick_s1
  g_sum_icc_choose_hockey_stick --> g_sum_icc_choose_hockey_stick_s2
  g_sum_icc_choose_hockey_stick --> g_sum_icc_choose_hockey_stick_s3
  cluster_open(["▸ open · 314"])
  class cluster_open open;
  click cluster_open call toggleCluster("open")
  cluster_translated(["▸ translated · 9"])
  class cluster_translated translated;
  click cluster_translated call toggleCluster("translated")
  cluster_proved(["▸ proved · 245"])
  class cluster_proved proved;
  click cluster_proved call toggleCluster("proved")
  cluster_archived(["▸ archived · 138"])
  class cluster_archived unknown;
  click cluster_archived call toggleCluster("archived")

All goals

Goal Status Diff Agent Solver / model PR Proved
abstract-regular-polyhedron-realizable-iffopen4—— ——
alt-sum-range-choose-sq-eq-zero-oddopen3—— ——
alt-sum-range-sq-eq-signed-pronicopen2—— ——
alt-sum-range-two-k-add-one-eq-signed-nopen2—— ——
alternating-sum-k-mul-choose-eq-zeroopen4—— ——
alternating-sum-shifted-choose-eq-oneopen4—— ——
am-gm-three-cubeopen3—— ——
am-hm-two-varopen2—— ——
cassini-nat-fib-intopen4—— ——
catalan-r2-int-fibopen2—— ——
catalan-r2-shift-nat-fib-intopen3—— ——
catalan-r3-shift-nat-fib-intopen3—— ——
cauchy-schwarz-three-var-productopen2—— ——
consecutive-fib-product-diff-nat-intopen4—— ——
cyclic-cube-sum-ge-asym-quad-cubicopen2—— ——
cyclotomic-five-divides-pow-five-sub-oneopen2—— ——
cyclotomic-three-divides-pow-six-sub-oneopen2—— ——
diff-tetrahedral-eq-triangularopen2—— ——
dvd-120-pow-eleven-sub-pow-threeopen3—— ——
dvd-1302-pow-thirtyone-sub-selfopen3—— ——
dvd-133-pow-nineteen-sub-selfopen2—— ——
dvd-1365-pow-fifteen-sub-pow-threeopen3—— ——
dvd-138-pow-twentythree-sub-selfopen3—— ——
dvd-170-pow-seventeen-sub-selfopen3—— ——
dvd-1806-pow-fortythree-sub-selfopen3—— ——
dvd-210-pow-fifteen-sub-pow-threeopen2—— ——
dvd-240-pow-nine-sub-pow-fiveopen3—— ——
dvd-252-pow-eight-sub-sqopen3—— ——
dvd-255-pow-seventeen-sub-selfopen3—— ——
dvd-266-pow-nineteen-sub-selfopen2—— ——
dvd-273-pow-fourteen-sub-sqopen2—— ——
dvd-273-pow-thirteen-sub-selfopen2—— ——
dvd-2730-pow-thirteen-sub-selfopen4—— ——
dvd-330-pow-twentythree-sub-pow-threeopen3—— ——
dvd-360-pow-fifteen-sub-pow-threeopen3—— ——
dvd-455-pow-fifteen-sub-pow-threeopen2—— ——
dvd-504-pow-nine-sub-pow-threeopen3—— ——
dvd-5040-seven-consecutive-productopen4—— ——
dvd-510-pow-fortynine-sub-pow-seventeenopen2—— ——
dvd-510-pow-nineteen-sub-pow-threeopen2—— ——
dvd-510-pow-thirtythree-sub-pow-seventeenopen3—— ——
dvd-510-pow-twentyone-sub-pow-fiveopen3—— ——
dvd-546-pow-fourteen-sub-sqopen2—— ——
dvd-630-pow-fourteen-sub-sqopen3—— ——
dvd-66-pow-thirtyone-sub-pow-elevenopen3—— ——
dvd-6765-pow-fortyone-sub-selfopen3—— ——
dvd-840-pow-fifteen-sub-pow-threeopen3—— ——
dvd-870-pow-twentynine-sub-selfopen3—— ——
dvd-903-pow-fortythree-sub-selfopen3—— ——
dvd-910-pow-thirteen-sub-selfopen2—— ——
dvd-910-pow-twentyfive-sub-pow-thirteenopen3—— ——
dvd-fortyeight-coprime-six-pow-four-sub-oneopen4—— ——
dvd-sixteen-odd-pow-four-sub-oneopen3—— ——
dvd-thirtytwo-odd-pow-eight-sub-oneopen3—— ——
eisenstein-norm-multiplicativeopen2—— ——
fib-add-five-eq-five-mul-fib-succ-add-three-mul-fibopen2—— ——
fib-add-four-eq-three-mul-fib-add-two-sub-fibopen2—— ——
fib-add-four-recurrence-natopen2—— ——
fib-add-six-eq-eight-mul-fib-succ-add-five-mul-fibopen2—— ——
fib-add-three-eq-two-mul-fib-succ-add-fibopen2—— ——
fib-add-two-sq-sub-fib-sq-eq-fib-two-mul-add-twoopen3—— ——
fib-consecutive-vieta-form-valueopen2—— ——
fib-prod-cross-shift-nat-intopen3—— ——
fib-two-mul-eq-fib-mul-two-mul-fib-succ-sub-fibopen3—— ——
fib-two-mul-sq-diff-intopen3—— ——
five-var-qm-amopen3—— ——
fourth-power-mod-fortyone-memopen2—— ——
hexagonal-eq-triangular-odd-indexopen1—— ——
lcm-self-succopen2—— ——
lucas-succ-add-lucas-pred-eq-five-mul-fibopen2—— ——
n4-plus-one-factor-over-sqrt-shiftopen2—— ——
nat-sq-lt-two-pow-s2open1—— ——
nesbitt-inequality-s1open1—— ——
nicomachus-sum-cubes-eq-sum-id-sqopen3—— ——
one-hundred-twenty-dvd-five-consecutiveopen3—— ——
platonic-pairs-realizableopen3—— ——
pow-five-add-pow-five-ge-quartic-mulopen3—— ——
prime-pow-eight-mod-480open4—— ——
prime-pow-six-mod-504open4—— ——
prod-icc-k-mul-add-two-div-succ-sq-telescopeopen3—— ——
prod-icc-k-mul-add-two-div-succ-sq-telescope-halfopen2—— ——
prod-icc-k-sq-div-pred-mul-succ-telescopeopen2—— ——
prod-icc-one-add-recip-eq-succopen2—— ——
prod-icc-one-add-recip-k-sq-add-two-k-telescopeopen3—— ——
prod-icc-one-add-recip-k-sq-sub-one-telescopeopen3—— ——
prod-icc-one-add-recip-pronicopen3—— ——
prod-icc-one-sub-recip-sq-eq-fracopen2—— ——
prod-icc-one-sub-two-div-pronicopen3—— ——
prod-icc-succ-add-three-div-self-eq-binom-shiftopen2—— ——
prod-icc-succ-sq-div-k-mul-add-two-telescopeopen2—— ——
prod-one-sub-inv-sq-telescopeopen4—— ——
prod-range-one-sub-recip-succ-sqopen2—— ——
quartic-n4-plus-four-compositeopen2—— ——
quartic-n4-plus-four-not-primeopen3—— ——
quartic-plus-four-not-primeopen4—— ——
quartic-sum-ge-abc-times-sumopen2—— ——
quartic-x4-plus-x2-plus-one-dvd-by-minus-factoropen2—— ——
realization-determines-countsopen5—— ——
realization-edge-in-setopen4—— ——
realization-edge-relationopen2—— ——
sextic-x6-plus-x3-plus-one-composite-shiftopen2—— ——
six-dvd-pow-three-add-five-mulopen2—— ——
sophie-germain-plus-factor-dvdopen2—— ——
sos-weighted-three-one-twoopen3—— ——
sq-add-sq-eq-three-mul-sq-s4open1—— ——
sq-mod-five-ne-two-threeopen2—— ——
sq-mod-ten-ne-two-three-seven-eightopen2—— ——
sum-centered-cube-eq-biquadraticopen2—— ——
sum-centered-hexagonal-eq-cubeopen2—— ——
sum-centered-octahedral-closed-formopen2—— ——
sum-centered-square-numbers-closed-formopen2—— ——
sum-centered-tetrahedral-closed-formopen2—— ——
sum-centered-triangular-closed-formopen2—— ——
sum-centered-triangular-running-closed-formopen2—— ——
sum-cube-add-id-closed-formopen2—— ——
sum-decagonal-closed-formopen3—— ——
sum-decagonal-numbers-closed-formopen2—— ——
sum-decagonal-second-kind-closed-formopen2—— ——
sum-even-cubes-eq-twice-squareopen2—— ——
sum-even-index-triangular-closed-formopen2—— ——
sum-even-squares-faulhaberopen2—— ——
sum-five-consecutive-product-closed-formopen2—— ——
sum-four-consecutive-eq-hyper-tetrahedralopen3—— ——
sum-fourth-powers-eqopen4—— ——
sum-fourth-powers-three-var-ge-sym-square-productsopen2—— ——
sum-heptagonal-closed-formopen3—— ——
sum-heptagonal-numbers-closed-formopen2—— ——
sum-hexagonal-eqopen3—— ——
sum-hexagonal-numbers-closed-formopen3—— ——
sum-icc-choose-hockey-stick-s1open1—— ——
sum-icc-choose-hockey-stick-s2open1—— ——
sum-icc-choose-hockey-stick-s3open1—— ——
sum-icc-cube-diff-recip-telescopeopen3—— ——
sum-icc-eight-k-div-odd-sq-pair-telescopeopen2—— ——
sum-icc-five-k-sub-two-mul-three-pow-pred-closedopen2—— ——
sum-icc-four-div-four-k-sub-one-four-k-add-three-telescopeopen2—— ——
sum-icc-four-div-three-consec-odd-telescopeopen2—— ——
sum-icc-id-mul-two-pow-predopen2—— ——
sum-icc-k-div-three-shifted-consecutive-telescopeopen3—— ——
sum-icc-k-mul-three-k-add-one-eqopen3—— ——
sum-icc-k-mul-three-k-sub-one-eqopen3—— ——
sum-icc-k-mul-two-k-sub-one-closed-formopen2—— ——
sum-icc-k-sq-add-one-mul-factorial-eq-prodopen3—— ——
sum-icc-k-sq-add-one-mul-factorial-eq-pronic-factorialopen2—— ——
sum-icc-k-sub-one-div-factorial-eq-one-subopen3—— ——
sum-icc-recip-four-consecutive-product-telescopeopen2—— ——
sum-icc-recip-k-sq-sub-one-telescopeopen3—— ——
sum-icc-recip-km1-k-kp1-telescopeopen3—— ——
sum-icc-recip-step-four-pair-eq-n-divopen2—— ——
sum-icc-three-div-three-k-sub-one-three-k-add-two-telescopeopen2—— ——
sum-icc-three-k-add-two-div-triple-consecutive-telescopeopen2—— ——
sum-icc-three-k-sub-one-mul-two-pow-pred-closedopen2—— ——
sum-icc-two-div-k-mul-k-add-two-telescopeopen2—— ——
sum-icc-two-k-add-one-div-k-sq-succ-sq-telescopeopen3—— ——
sum-id-mul-triangular-closed-formopen3—— ——
sum-k-add-one-mul-two-powopen2—— ——
sum-k-mul-k-add-two-closed-formopen2—— ——
sum-k-mul-succ-mul-two-k-succopen3—— ——
sum-k-mul-succ-sq-closed-formopen2—— ——
sum-k-sq-mul-succ-closed-formopen2—— ——
sum-k-sq-mul-two-powopen3—— ——
sum-nonagonal-closed-formopen3—— ——
sum-nonagonal-numbers-closed-formopen2—— ——
sum-oblong-eqopen2—— ——
sum-octagonal-eqopen3—— ——
sum-octagonal-numbers-closed-formopen2—— ——
sum-octagonal-running-closed-formopen3—— ——
sum-octahedral-centered-squaresopen2—— ——
sum-octahedral-numbers-closed-formopen2—— ——
sum-odd-gnomon-squares-closed-formopen3—— ——
sum-odd-squares-eqopen3—— ——
sum-odd-squares-faulhaberopen2—— ——
sum-one-div-four-k-plus-one-mul-four-k-plus-fiveopen3—— ——
sum-one-div-succ-mul-add-four-telescopeopen4—— ——
sum-one-div-three-k-plus-one-mul-three-k-plus-fouropen3—— ——
sum-pentagonal-eqopen3—— ——
sum-pentagonal-pyramidal-closed-formopen3—— ——
sum-pentagonal-running-eq-pyramidalopen3—— ——
sum-pentatope-triple-productopen2—— ——
sum-product-consecutive-odds-closed-formopen2—— ——
sum-pronic-eq-thrice-tetrahedralopen2—— ——
sum-quadruple-product-closed-formopen2—— ——
sum-quintic-gnomon-eq-fifth-poweropen2—— ——
sum-range-catalan-mul-catalan-eq-catalan-succopen3—— ——
sum-range-choose-mul-choose-three-eqopen4—— ——
sum-range-choose-mul-k-mul-comp-eqopen4—— ——
sum-range-choose-mul-succ-choose-eqopen3—— ——
sum-range-choose-mul-succ-choose-succ-eq-central-shiftopen3—— ——
sum-range-choose-sq-eq-centralopen4—— ——
sum-range-comp-mul-choose-sq-eqopen3—— ——
sum-range-compositions-count-eq-two-powopen3—— ——
sum-range-cube-diff-eq-cubeopen2—— ——
sum-range-cube-mul-three-pow-closedopen3—— ——
sum-range-cube-mul-two-pow-closedopen3—— ——
sum-range-cube-sym-choose-sq-eq-zeroopen4—— ——
sum-range-disp-mul-choose-eq-zeroopen2—— ——
sum-range-disp-mul-choose-sq-eq-zeroopen3—— ——
sum-range-even-cols-eq-two-powopen4—— ——
sum-range-fall-three-mul-chooseopen4—— ——
sum-range-fib-mul-two-pow-rev-eqopen3—— ——
sum-range-fib-prod-shift-even-natopen3—— ——
sum-range-fib-sq-eq-fib-mul-fib-succopen3—— ——
sum-range-fib-sq-eq-prodopen3—— ——
sum-range-fib-sq-mul-two-eqopen3—— ——
sum-range-fib-two-mul-succ-eq-fib-predopen3—— ——
sum-range-four-consecutive-productopen3—— ——
sum-range-four-cube-diff-eqopen2—— ——
sum-range-four-mul-add-oneopen2—— ——
sum-range-half-even-row-choose-eqopen3—— ——
sum-range-id-div-two-powopen3—— ——
sum-range-id-div-two-pow-eq-two-subopen3—— ——
sum-range-id-mul-add-twoopen3—— ——
sum-range-id-mul-choose-eq-halfopen3—— ——
sum-range-id-mul-four-pow-closedopen2—— ——
sum-range-id-mul-neg-two-pow-closedopen2—— ——
sum-range-id-mul-succ-mul-two-pow-closedopen3—— ——
sum-range-id-mul-three-powopen3—— ——
sum-range-id-mul-three-pow-closedopen2—— ——
sum-range-k-div-succ-factorial-eqopen3—— ——
sum-range-k-div-succ-factorial-telescopeopen3—— ——
sum-range-k-mul-choose-mul-four-pow-closedopen3—— ——
sum-range-k-mul-choose-mul-three-pow-closedopen3—— ——
sum-range-k-mul-choose-mul-two-pow-eq-two-n-three-powopen3—— ——
sum-range-k-mul-choose-sq-eq-centralopen4—— ——
sum-range-k-mul-factorial-eq-factorial-succ-sub-oneopen3—— ——
sum-range-k-mul-factorial-succopen3—— ——
sum-range-k-mul-two-pow-eqopen2—— ——
sum-range-k-plus-one-mul-chooseopen3—— ——
sum-range-k-sq-mul-choose-eqopen3—— ——
sum-range-k-sq-mul-five-pow-closedopen2—— ——
sum-range-k-sq-mul-four-pow-closedopen2—— ——
sum-range-k-sub-one-div-factorial-telescopeopen2—— ——
sum-range-lower-triangle-choose-eq-two-powopen3—— ——
sum-range-lucas-shift-natopen3—— ——
sum-range-multichoose-two-eq-choose-succ-twoopen2—— ——
sum-range-odd-cubesopen3—— ——
sum-range-odd-div-two-powopen3—— ——
sum-range-odd-index-choose-eq-two-powopen3—— ——
sum-range-odd-mul-three-powopen3—— ——
sum-range-odd-num-sq-succ-sq-telescopeopen3—— ——
sum-range-pascal-diagonal-eq-chooseopen3—— ——
sum-range-recip-choose-two-eq-two-n-div-succopen3—— ——
sum-range-recip-consecutiveopen3—— ——
sum-range-recip-five-step-productopen3—— ——
sum-range-recip-five-step-residue-oneopen2—— ——
sum-range-recip-four-consec-productopen3—— ——
sum-range-recip-four-step-productopen2—— ——
sum-range-recip-four-step-residue-oneopen2—— ——
sum-range-recip-odd-consecutiveopen2—— ——
sum-range-recip-odd-pair-consecutiveopen2—— ——
sum-range-recip-odd-pair-step-two-eq-n-divopen2—— ——
sum-range-recip-odd-productopen3—— ——
sum-range-recip-shift-two-shift-five-telescopeopen3—— ——
sum-range-recip-three-consec-odd-telescopeopen3—— ——
sum-range-recip-three-consec-shiftedopen3—— ——
sum-range-recip-three-consecutiveopen3—— ——
sum-range-recip-three-step-residue-oneopen2—— ——
sum-range-recip-triple-consecutiveopen3—— ——
sum-range-recip-two-powopen2—— ——
sum-range-shifted-choose-eq-two-pow-sub-oneopen3—— ——
sum-range-sq-add-one-mul-two-pow-closedopen3—— ——
sum-range-sq-mul-four-pow-closedopen3—— ——
sum-range-sq-mul-three-powopen2—— ——
sum-range-sq-mul-three-pow-closedopen3—— ——
sum-range-sq-mul-two-powopen2—— ——
sum-range-stirling-first-row-eq-factorialopen3—— ——
sum-range-succ-div-factorial-add-two-telescopeopen3—— ——
sum-range-succ-div-two-pow-eq-four-subopen3—— ——
sum-range-succ-k-mul-choose-mul-two-pow-closedopen3—— ——
sum-range-succ-mul-choose-sq-eqopen3—— ——
sum-range-succ-mul-factorial-eqopen2—— ——
sum-range-succ-mul-factorial-succopen2—— ——
sum-range-succ-mul-two-pow-eq-closedopen2—— ——
sum-range-succ-sq-mul-two-pow-closedopen3—— ——
sum-range-three-k-add-two-mul-two-pow-closedopen2—— ——
sum-range-three-mul-add-oneopen2—— ——
sum-range-triangular-eq-tetrahedralopen3—— ——
sum-range-two-k-add-one-div-two-pow-closedopen3—— ——
sum-range-two-k-add-one-mul-two-pow-closedopen3—— ——
sum-range-two-k-sub-n-mul-choose-sq-eq-zeroopen3—— ——
sum-range-two-k-sub-one-mul-three-pow-closedopen2—— ——
sum-range-two-k-succ-mul-choose-eqopen2—— ——
sum-range-two-mul-add-oneopen2—— ——
sum-range-vandermonde-self-eq-central-chooseopen3—— ——
sum-range-window-five-fib-eq-fib-diff-natopen2—— ——
sum-range-window-four-fib-eq-fib-diff-natopen2—— ——
sum-recip-times-sum-ge-nineopen3—— ——
sum-rhombic-dodecahedral-eq-fourth-poweropen2—— ——
sum-sixth-ge-mixed-fourth-secondopen2—— ——
sum-square-pyramidal-eq-hyperopen3—— ——
sum-squares-eq-square-pyramidalopen2—— ——
sum-star-numbers-closed-formopen2—— ——
sum-stella-octangula-closed-formopen2—— ——
sum-tetrahedral-eq-pentatopeopen3—— ——
sum-three-squares-zmod-eight-ne-sevenopen3—— ——
sum-three-squares-zmod-sixteen-ne-fifteenopen3—— ——
sum-triangular-squared-closed-formopen3—— ——
sum-triple-product-eqopen3—— ——
sum-two-cubes-zmod-nine-ne-fouropen3—— ——
sum-two-cubes-zmod-seven-memopen3—— ——
sum-two-fourth-powers-zmod-sixteen-memopen3—— ——
sum-two-k-add-one-mul-two-powopen2—— ——
sum-two-k-plus-one-div-sq-succ-sq-telescopeopen3—— ——
sum-two-k-sub-one-mul-two-powopen2—— ——
sum-two-squares-zmod-eight-ne-sixopen3—— ——
sum-two-squares-zmod-four-ne-threeopen2—— ——
sum-vandermonde-diagonal-eq-chooseopen3—— ——
sumsq-ge-ab-plus-bcopen2—— ——
sumsq-products-ge-abc-times-sumopen2—— ——
sym-deg-three-ge-six-mulopen3—— ——
sym-grouped-deg-three-ge-six-abcopen3—— ——
tangent-line-cube-trickopen3—— ——
three-cubes-minus-three-prod-dvd-sumopen2—— ——
three-cubes-zmod-nine-ne-four-fiveopen2—— ——
three-fourth-powers-zmod-sixteen-memopen3—— ——
three-mul-fib-eq-fib-add-two-add-fib-sub-twoopen2—— ——
three-quartic-sum-ge-sumsq-sqopen3—— ——
two-cubes-zmod-nine-ne-three-four-five-sixopen2—— ——
two-fib-add-intopen3—— ——
two-fourth-powers-zmod-five-ne-three-fouropen2—— ——
two-mul-sum-icc-three-k-sub-two-eq-pentagonalopen2—— ——
two-mul-sum-range-fib-triple-eq-fib-predopen4—— ——
two-squares-zmod-sixteen-ne-three-seven-elevenopen2—— ——
two-sum-cubes-ge-sym-quadraticsopen3—— ——
nesbitt-inequalityblocked4—— ——
sq-add-sq-eq-three-mul-sqblocked4—— ——
sum-icc-choose-hockey-stickblocked3—— ——
nat-add-assoctranslated——— ——
nat-add-zerotranslated——— ——
nat-le-refltranslated——— ——
nat-le-transtranslated——— ——
nat-leq-selftranslated——— ——
nat-mul-commtranslated——— ——
nat-mul-onetranslated——— ——
nat-product-ordertranslated——— ——
nat-zero-identity-addtranslated——— ——
abc-nine-le-sum-times-pairsumproved3claude-rmt-001chat-bit-01 #11482026-06-17
am-gm-three-cube-s1proved11367ab40f0b1-e413cgbarlow #6112026-06-15
am-gm-three-cube-s2proved1oma-2-c50dperttu-mp · opus#12022026-06-16
am-gm-three-cube-s2-s1proved1oma-2-c50dperttu · gemini-3.1-pro-preview#4962026-06-14
am-gm-three-cube-s2-s2proved1claude-rmt-001chat-bit-01 #11312026-06-16
am-gm-three-cube-s2-s2-s1proved11367ab40f0b1-e413cgbarlow · opus#6492026-06-15
am-gm-three-cube-s2-s2-s2proved11367ab40f0b1-e413cgbarlow · opus#6442026-06-15
am-hm-two-var-s1proved1claude-rmt-001perttu · gemini-3.1-pro-preview#7132026-06-15
am-hm-two-var-s2proved1oma-2-c50dperttu · gemini-3.1-pro-preview#6522026-06-15
am-hm-two-var-s3proved11367ab40f0b1-e413cgbarlow · opus#6462026-06-15
amgm-four-cross-three-varproved3thebeast-ace7adam91holt #6782026-06-15
amgm-prod-half-sum-le-cubesproved3claude-rmt-001chat-bit-01 #11412026-06-17
bezout-eleven-thirteen-eq-oneproved2claude-rmt-001chat-bit-01 #9852026-06-16
bezout-five-seven-eq-oneproved2claude-rmt-001chat-bit-01 #9842026-06-15
candido-sum-quartics-twice-squareproved2claude-rmt-001chat-bit-01 #11392026-06-16
cauchy-schwarz-two-termproved2claude-rmt-001chat-bit-01 #11102026-06-16
consec-prod-succ-coprimeproved21367ab40f0b1-e413cgbarlow · opus#9672026-06-15
constrained-pairsum-le-three-sum-threeproved2afnz-zbook-b336cgbarlow · leanstral-2603#8422026-06-15
constrained-prod-le-sum-cubes-thirdproved21367ab40f0b1-e413cgbarlow · opus#9652026-06-15
constrained-sum-le-sumsq-prod-oneproved21367ab40f0b1-e413cgbarlow · opus#9662026-06-15
constrained-sum-sq-ge-one-thirdproved2claude-rmt-001chat-bit-01 #11332026-06-16
constrained-sum-sq-ge-threeproved21367ab40f0b1-e413cgbarlow · opus#6332026-06-15
coprime-2n1-2n3proved2claude-rmt-001chat-bit-01 #8922026-06-15
coprime-2n1-3n2proved21367ab40f0b1-e413cgbarlow · opus#6802026-06-15
coprime-2n1-n1proved31367ab40f0b1-e413cgbarlow · opus#6192026-06-15
coprime-3n1-4n1proved2claude-rmt-001chat-bit-01 #8882026-06-15
coprime-consec-triproved3claude-rmt-001chat-bit-01 #10062026-06-16
coprime-fib-sq-fib-succproved3claude-rmt-001chat-bit-01 #10162026-06-16
coprime-n-cube-add-oneproved2claude-rmt-001chat-bit-01 #9412026-06-15
coprime-n-sq-n-add-oneproved2afnz-zbook-b336cgbarlow · leanstral-2603#7182026-06-15
coprime-n1-nsq1proved3claude-rmt-001chat-bit-01 #9472026-06-15
coprime-n2p1-n2p2proved2claude-rmt-001chat-bit-01 #9402026-06-15
coprime-ncube1-ncube2proved2claude-rmt-001chat-bit-01 #9522026-06-15
coprime-nsq2-nsq3proved2claude-rmt-001chat-bit-01 #9452026-06-15
coprime-succ-sq-addproved3claude-rmt-001chat-bit-01 #9342026-06-16
coprime-twopow-sub-one-twoproved3claude-rmt-001chat-bit-01 #10112026-06-16
cube-mod-eighteen-memproved3claude-rmt-001chat-bit-01 #7842026-06-15
cube-mod-fortythree-memproved31367ab40f0b1-e413cgbarlow · opus#9682026-06-15
cube-mod-fourteen-memproved2claude-rmt-001chat-bit-01 #10192026-06-16
cube-mod-nineproved21367ab40f0b1-e413cgbarlow · opus#6202026-06-15
cube-mod-nineteen-memproved3claude-rmt-001chat-bit-01 #10202026-06-16
cube-mod-thirteen-memproved31367ab40f0b1-e413cgbarlow · opus#6252026-06-15
cube-mod-thirtyone-nonresidue-fiveproved3afnz-zbook-b336cgbarlow · leanstral-2603#7772026-06-15
cube-mod-thirtyseven-memproved31367ab40f0b1-e413cgbarlow · opus#9702026-06-15
cube-mod-twentyone-memproved2afnz-zbook-b336cgbarlow · leanstral-2603#8442026-06-15
cube-mod-twentyseven-memproved3afnz-zbook-b336cgbarlow · leanstral-2603#8112026-06-15
cube-mod-twentysix-memproved3claude-rmt-001chat-bit-01 #10222026-06-16
cube-of-sum-minus-cubes-div-by-sumproved2claude-rmt-001chat-bit-01 #11372026-06-16
cube-sum-ge-three-prodproved2oma-2-c50dperttu #11702026-06-16
cube-sum-ge-three-prod-s1proved1claude-rmt-001chat-bit-01 #6982026-06-15
cube-sum-ge-three-prod-s2proved1claude-rmt-001chat-bit-01 #11352026-06-16
cube-sum-ge-three-prod-s3proved1afnz-zbook-b336cgbarlow · leanstral-2603#4932026-06-14
cyclic-quad-ge-abc-times-sumproved3claude-rmt-001chat-bit-01 #11442026-06-17
cyclic-quartic-ge-asym-cubic-crossproved21367ab40f0b1-e413cgbarlow · opus#9732026-06-15
diff-sixth-power-dvd-by-sumproved2afnz-zbook-b336cgbarlow · leanstral-2603#8652026-06-15
diff-twelfth-power-dvd-by-diff-cubeproved2claude-rmt-001chat-bit-01 #11402026-06-16
diff-two-cubes-zmod-seven-ne-three-fourproved2claude-rmt-001chat-bit-01 #11002026-06-16
diff-two-squares-zmod-four-ne-twoproved2claude-rmt-001chat-bit-01 #10962026-06-16
diff-two-squares-zmod-sixteen-ne-two-sixproved21367ab40f0b1-e413cgbarlow · opus#9752026-06-15
discriminant-nonnegproved3oma-2-c50dperttu · gemini-3.1-pro-preview#6652026-06-15
discriminant-nonneg-s1proved1claude-rmt-001cgbarlow · opus#7102026-06-15
discriminant-nonneg-s2proved1claude-rmt-001cgbarlow · opus#6692026-06-15
discriminant-nonneg-s3proved11367ab40f0b1-e413cgbarlow · opus#6272026-06-15
dvd-1023-pow-thirtyone-sub-selfproved3mac-158fohdearquant · template-zmod-crt#12272026-06-16
dvd-120-five-consecutive-productproved31367ab40f0b1-e413cgbarlow · opus#9772026-06-15
dvd-120-pow-seven-sub-pow-threeproved3claude-rmt-001chat-bit-01 #11612026-06-17
dvd-1365-pow-thirteen-sub-selfproved2mac-158fohdearquant · template-zmod-crt#12342026-06-17
dvd-138-pow-fortyfive-sub-pow-twentythreeproved21367ab40f0b1-e413cgbarlow · opus#9782026-06-15
dvd-210-pow-fifteen-sub-pow-three-s1proved1mac-158fohdearquant · template-zmod-decide#12072026-06-16
dvd-210-pow-fifteen-sub-pow-three-s2proved1mac-158fohdearquant · template-zmod-decide#12082026-06-16
dvd-210-pow-fifteen-sub-pow-three-s3proved1oma-2-c50dperttu #8902026-06-15
dvd-210-pow-fifteen-sub-pow-three-s4proved1mac-158fohdearquant · template-zmod-decide#12092026-06-16
dvd-240-pow-eight-sub-pow-fourproved3mac-158fohdearquant · template-zmod-crt#12382026-06-16
dvd-264-pow-thirteen-sub-pow-threeproved3oma-2-c50dperttu #8842026-06-15
dvd-282-pow-fortyseven-sub-selfproved3mac-158fohdearquant · template-zmod-crt#12462026-06-17
dvd-30-pow-nine-sub-selfproved31367ab40f0b1-e413cgbarlow · opus#6282026-06-15
dvd-30-pow-twentyone-sub-pow-fiveproved2mac-158fohdearquant · template-zmod-decide#12102026-06-16
dvd-330-pow-twentyone-sub-selfproved3oma-2-c50dperttu #7542026-06-15
dvd-399-pow-nineteen-sub-selfproved2mac-158fohdearquant · template-zmod-crt#12492026-06-17
dvd-42-pow-twentyfive-sub-pow-sevenproved2mac-158fohdearquant · template-zmod-decide#12112026-06-16
dvd-455-pow-thirteen-sub-selfproved2oma-2-c50dperttu #9122026-06-15
dvd-462-pow-thirtyone-sub-selfproved3oma-2-c50dperttu · opus#9142026-06-15
dvd-480-pow-thirteen-sub-pow-fiveproved3mac-158fohdearquant · template-zmod-crt#12512026-06-17
dvd-510-pow-seventeen-sub-selfproved3oma-2-c50dperttu #7702026-06-15
dvd-66-pow-eleven-sub-selfproved31367ab40f0b1-e413cgbarlow · opus#6292026-06-15
dvd-66-pow-twentyone-sub-pow-elevenproved3oma-2-c50dperttu · opus#9292026-06-15
dvd-798-pow-nineteen-sub-selfproved3oma-2-c50dperttu #7672026-06-15
dvd-798-pow-thirtyseven-sub-pow-nineteenproved3mac-158fohdearquant · template-zmod-crt#12622026-06-17
dvd-910-pow-fifteen-sub-pow-threeproved3mac-158fohdearquant · template-zmod-crt#12672026-06-17
dvd-nine-pow-nine-sub-pow-threeproved31367ab40f0b1-e413cgbarlow · opus#6302026-06-15
dvd-sixty-pow-six-sub-sqproved2mac-158fohdearquant · template-zmod-decide#12122026-06-16
dvd-sixty-pow-ten-sub-sqproved2mac-158fohdearquant · template-zmod-decide#12132026-06-16
dvd-twentyfour-pow-five-sub-pow-threeproved2mac-158fohdearquant · template-zmod-decide#12142026-06-16
dvd-twentyfour-pow-seven-sub-pow-fiveproved2mac-158fohdearquant · template-zmod-decide#12152026-06-16
dvd-twentyfour-pow-six-sub-pow-fourproved2mac-158fohdearquant · template-zmod-decide#12162026-06-16
eight-sum-pow-four-ge-sum-pow-fourproved31367ab40f0b1-e413cgbarlow · opus#6312026-06-15
eighth-power-mod-fifteen-memproved2claude-rmt-001chat-bit-01 #8592026-06-15
eighth-power-mod-seventeen-memproved3claude-rmt-001chat-bit-01 #10272026-06-16
eighth-power-mod-sixteen-memproved2claude-rmt-001chat-bit-01 #10342026-06-16
eighth-power-mod-thirtytwo-memproved2claude-rmt-001chat-bit-01 #10352026-06-16
eleventh-power-mod-twentythree-memproved2claude-rmt-001chat-bit-01 #10312026-06-16
fifth-power-mod-elevenproved21367ab40f0b1-e413cgbarlow · opus#6322026-06-15
fifth-power-mod-sixteen-odd-memproved3claude-rmt-001chat-bit-01 #10332026-06-16
fifth-power-mod-twentytwo-memproved3claude-rmt-001chat-bit-01 #10242026-06-16
four-not-dvd-sq-add-twoproved31367ab40f0b1-e413cgbarlow · opus#6342026-06-15
four-var-cyclic-sosproved2oma-2-c50dperttu · gemini-3.1-pro-preview#6392026-06-15
four-var-qm-amproved2mac-158fohdearquant · sonnet#11762026-06-16
four-var-qm-am-s1proved1oma-2-c50dperttu #7512026-06-15
four-var-qm-am-s2proved1claude-rmt-001chat-bit-01 #11202026-06-16
four-var-qm-am-s3proved1afnz-zbook-b336cgbarlow · leanstral-2603#6962026-06-15
fourth-power-mod-eight-memproved3afnz-zbook-b336cgbarlow · leanstral-2603#6402026-06-15
fourth-power-mod-eighty-memproved3claude-rmt-001chat-bit-01 #10382026-06-16
fourth-power-mod-five-memproved1claude-rmt-001chat-bit-01 #8312026-06-15
fourth-power-mod-fortyeight-memproved3claude-rmt-001chat-bit-01 #10362026-06-16
fourth-power-mod-hundred-memproved3claude-rmt-001chat-bit-01 #10392026-06-16
fourth-power-mod-nine-memproved2claude-rmt-001chat-bit-01 #8412026-06-15
fourth-power-mod-ten-memproved2claude-rmt-001chat-bit-01 #8362026-06-15
fourth-power-mod-thirteen-memproved3claude-rmt-001cgbarlow · opus#7692026-06-15
fourth-power-mod-thirtytwo-memproved3claude-rmt-001chat-bit-01 #10252026-06-16
fourth-power-mod-twentyfive-memproved2claude-rmt-001chat-bit-01 #10232026-06-16
gcd-2n1-2n5-dvd-fourproved2claude-rmt-001chat-bit-01 #8792026-06-15
gcd-2n1-2n7-dvd-sixproved2claude-rmt-001chat-bit-01 #8832026-06-15
gcd-2n1-3n4-dvd-fiveproved3claude-rmt-001chat-bit-01 #8812026-06-15
gcd-2n3-3n5-eq-oneproved2claude-rmt-001chat-bit-01 #9762026-06-15
gcd-2n3-4n5-dvd-twoproved3claude-rmt-001chat-bit-01 #9902026-06-16
gcd-2n5-3n7-eq-oneproved3claude-rmt-001chat-bit-01 #8632026-06-15
gcd-2pow-3pow-eq-oneproved2claude-rmt-001chat-bit-01 #10082026-06-16
gcd-3n1-5n2-eq-oneproved2claude-rmt-001chat-bit-01 #9712026-06-15
gcd-3n1-9n4-eq-oneproved2claude-rmt-001chat-bit-01 #9812026-06-15
gcd-3n2-4n3-eq-oneproved3claude-rmt-001chat-bit-01 #8612026-06-15
gcd-3n2-5n4-dvd-twoproved2claude-rmt-001chat-bit-01 #9882026-06-16
gcd-3n4-5n7-eq-oneproved3claude-rmt-001chat-bit-01 #9582026-06-15
gcd-4n1-6n1-dvd-twoproved3claude-rmt-001chat-bit-01 #8872026-06-15
gcd-4n3-5n4-eq-oneproved2claude-rmt-001chat-bit-01 #9792026-06-15
gcd-4n3-6n5-eq-oneproved3claude-rmt-001chat-bit-01 #8002026-06-15
gcd-5n2-7n3-eq-oneproved3claude-rmt-001chat-bit-01 #7942026-06-15
gcd-5n3-7n4-eq-oneproved2—— —2026-06-15
gcd-6n5-4n3-eq-oneproved3claude-rmt-001chat-bit-01 #9602026-06-15
gcd-6n5-6n11-eq-oneproved2claude-rmt-001chat-bit-01 #9642026-06-15
gcd-consec-odd-eq-oneproved3claude-rmt-001chat-bit-01 #9862026-06-16
gcd-factorial-succ-eq-factorialproved3claude-rmt-001chat-bit-01 #10152026-06-16
gcd-fib-add-two-eq-gcd-fib-succproved3claude-rmt-001chat-bit-01 #10172026-06-16
gcd-lin-3n2-5n3proved31367ab40f0b1-e413cgbarlow · opus#6582026-06-15
gcd-n-add-six-dvd-sixproved2claude-rmt-001chat-bit-01 #8692026-06-15
gcd-n-factorial-succ-eq-oneproved3claude-rmt-001chat-bit-01 #10092026-06-16
gcd-n1-n7-dvd-sixproved2claude-rmt-001chat-bit-01 #8722026-06-15
gcd-n2-2n5-eq-oneproved2claude-rmt-001chat-bit-01 #8662026-06-15
gcd-n2-n4-dvd-twoproved2claude-rmt-001chat-bit-01 #8702026-06-15
gcd-n2-n6-dvd-fourproved2claude-rmt-001chat-bit-01 #8742026-06-15
gcd-n2-n8-dvd-sixproved2claude-rmt-001chat-bit-01 #8762026-06-15
gcd-n2p1-n2p3-dvd-twoproved2claude-rmt-001chat-bit-01 #9922026-06-16
gcd-n3-2n7-eq-oneproved2claude-rmt-001chat-bit-01 #9542026-06-15
gcd-n3p1-np1-eq-np1proved2claude-rmt-001chat-bit-01 #10002026-06-16
gcd-n4p1-n2p1-dvd-twoproved2claude-rmt-001chat-bit-01 #10032026-06-16
gcd-np1-2np1-eq-oneproved2claude-rmt-001chat-bit-01 #8672026-06-15
gcd-np1-n2p1-dvd-twoproved2claude-rmt-001chat-bit-01 #10012026-06-16
gcd-nsq1-n1-dvd-twoproved3claude-rmt-001chat-bit-01 #9962026-06-16
gcd-nsq1-nsq3-dvd-twoproved2claude-rmt-001chat-bit-01 #9512026-06-15
gcd-quad-factored-n1-eq-n1proved3claude-rmt-001chat-bit-01 #10022026-06-16
gcd-sq-n-sq-n-oneproved3claude-rmt-001chat-bit-01 #9972026-06-16
gcd-three-pow-succ-three-pow-add-oneproved3claude-rmt-001chat-bit-01 #10132026-06-16
gcd-threen-n7-dvd-twentyoneproved3claude-rmt-001chat-bit-01 #9952026-06-16
gcd-two-pow-add-one-sub-one-dvd-twoproved3claude-rmt-001chat-bit-01 #10072026-06-16
gcd-twon-n5-dvd-tenproved3claude-rmt-001chat-bit-01 #9942026-06-16
nat-sq-lt-two-powproved3—adam91holt · gpt-5.5—2026-06-14
nat-sq-lt-two-pow-s1proved1oma-2-c50dperttu #4422026-06-14
nat-sq-lt-two-pow-s2-s1proved11367ab40f0b1-e413cgbarlow · opus#6662026-06-15
nat-sq-lt-two-pow-s2-s2proved1—adam91holt · gpt-5.5—2026-06-14
nat-sq-lt-two-pow-s2-s3proved1—adam91holt · gpt-5.5—2026-06-14
nat-zero-lt-succproved——— —2026-06-10
nesbitt-inequality-s2proved1claude-rmt-001chat-bit-01 #4512026-06-14
nesbitt-inequality-s3proved1afnz-zbook-b336cgbarlow · leanstral-2603#6672026-06-15
nesbitt-inequality-s4proved11367ab40f0b1-e413cgbarlow · opus#6682026-06-15
ninth-power-mod-nineteen-memproved2claude-rmt-001chat-bit-01 #10292026-06-16
no-int-sq-eq-eight-mul-add-threeproved3claude-rmt-001chat-bit-01 #7912026-06-15
no-nat-sq-eq-two-mul-sqproved4oma-2-c50dperttu #7472026-06-15
no-nat-sq-eq-two-mul-sq-s1proved11367ab40f0b1-e413cgbarlow · opus#6702026-06-15
no-nat-sq-eq-two-mul-sq-s2proved11367ab40f0b1-e413cgbarlow · opus#6712026-06-15
no-nat-sq-eq-two-mul-sq-s3proved1thebeast-ace7adam91holt #6732026-06-15
no-nat-sq-eq-two-mul-sq-s4proved1claude-rmt-001chat-bit-01 #4402026-06-14
numderangements-add-two-int-formproved2oma-2-c50dperttu #10642026-06-16
pair-sum-sq-ge-three-abc-sumproved2claude-rmt-001chat-bit-01 #11152026-06-16
pairwise-product-sum-sq-ge-three-abc-sumproved3claude-rmt-001chat-bit-01 #11172026-06-16
pell-brahmagupta-composition-d2proved3oma-2-c50dperttu · opus#10732026-06-16
pell-brahmagupta-composition-generic-dproved3claude-rmt-001chat-bit-01 #10742026-06-16
pell-d10-fundamental-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10462026-06-16
pell-d11-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10422026-06-16
pell-d12-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10442026-06-16
pell-d13-ladder-step-preservesproved3claude-rmt-001chat-bit-01 #10452026-06-16
pell-d14-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10472026-06-16
pell-d15-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10482026-06-16
pell-d17-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10502026-06-16
pell-d18-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10522026-06-16
pell-d2-convergent-cross-differenceproved2oma-2-c50dperttu · opus#10752026-06-16
pell-d2-form-product-telescope-stepproved2claude-rmt-001chat-bit-01 #10722026-06-16
pell-d2-ladder-cross-determinantproved2oma-2-c50dperttu · opus#10762026-06-16
pell-d2-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10402026-06-16
pell-d2-negative-seven-ladder-preservesproved2afnz-zbook-b336cgbarlow · leanstral-2603#10802026-06-16
pell-d2-negative-to-positive-stepproved2claude-rmt-001chat-bit-01 #10792026-06-16
pell-d2-no-small-nontrivial-yproved3claude-rmt-001chat-bit-01 #11022026-06-16
pell-d2-positive-multiple-of-formproved2claude-rmt-001chat-bit-01 #10772026-06-16
pell-d2-positive-to-negative-stepproved2claude-rmt-001chat-bit-01 #10822026-06-16
pell-d2-quad-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10622026-06-16
pell-d2-rational-bound-aboveproved2oma-2-c50dperttu #10842026-06-16
pell-d2-rational-bound-gapproved2afnz-zbook-b336cgbarlow · leanstral-2603#10862026-06-16
pell-d2-solution-coords-coprimeproved2claude-rmt-001chat-bit-01 #11072026-06-16
pell-d2-square-doubling-identityproved2claude-rmt-001chat-bit-01 #10682026-06-16
pell-d2-square-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10602026-06-16
pell-d2-stormer-seven-ladder-preservesproved2claude-rmt-001chat-bit-01 #10852026-06-16
pell-d2-x-oddproved3claude-rmt-001chat-bit-01 #10982026-06-16
pell-d2-x-sq-congr-one-mod-eightproved2claude-rmt-001chat-bit-01 #11062026-06-16
pell-d2-y-evenproved3oma-2-c50dperttu #10942026-06-16
pell-d2-y-lt-x-of-posproved2afnz-zbook-b336cgbarlow · leanstral-2603#10992026-06-16
pell-d21-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10542026-06-16
pell-d23-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10562026-06-16
pell-d3-form-value-ne-two-zmod3proved2claude-rmt-001chat-bit-01 #10922026-06-16
pell-d3-fundamental-square-doublingproved2claude-rmt-001chat-bit-01 #10702026-06-16
pell-d3-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10412026-06-16
pell-d3-no-negative-solution-zmod3proved3claude-rmt-001chat-bit-01 #10932026-06-16
pell-d3-no-small-nontrivial-yproved3claude-rmt-001chat-bit-01 #11082026-06-16
pell-d3-rational-bound-aboveproved2claude-rmt-001chat-bit-01 #11042026-06-16
pell-d3-x-coord-pos-gt-yproved3claude-rmt-001chat-bit-01 #11012026-06-16
pell-d5-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10572026-06-16
pell-d5-negative-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10652026-06-16
pell-d5-positive-from-negative-squareproved2claude-rmt-001chat-bit-01 #10902026-06-16
pell-d6-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10582026-06-16
pell-d7-ladder-step-preservesproved2claude-rmt-001chat-bit-01 #10592026-06-16
pell-d7-no-negative-solution-zmod7proved2claude-rmt-001chat-bit-01 #10952026-06-16
pell-doubling-identity-generic-dproved3claude-rmt-001chat-bit-01 #10872026-06-16
pell-negative-brahmagupta-composition-generic-dproved2claude-rmt-001chat-bit-01 #10892026-06-16
pow-four-add-pow-four-ge-cube-mulproved2claude-rmt-001chat-bit-01 #11492026-06-17
product-of-two-sums-of-squares-ge-square-of-crossproved2claude-rmt-001chat-bit-01 #11502026-06-17
quad-form-divides-cube-sumproved1claude-rmt-001chat-bit-01 #11272026-06-16
quad-form-ge-three-quarter-sqproved2claude-rmt-001chat-bit-01 #11562026-06-17
quartic-n4-plus-four-dvd-by-shift-quadraticproved2afnz-zbook-b336cgbarlow · leanstral-2603#11642026-06-16
quartic-x4-plus-64-dvd-by-x2-minus-4x-plus-8proved2afnz-zbook-b336cgbarlow · leanstral-2603#11682026-06-16
shifted-sophie-germain-x4-plus-4-dvd-by-x2-plus-2x-plus-2proved2claude-rmt-001chat-bit-01 #11532026-06-17
shifted-sum-sq-ge-twice-sum-three-varproved2claude-rmt-001chat-bit-01 #11142026-06-16
six-dvd-n-mul-succ-mul-two-n-add-oneproved2mac-158fohdearquant · template-zmod-decide#12172026-06-16
six-dvd-pow-three-add-five-mul-s1proved1afnz-zbook-b336cgbarlow · leanstral-2603#12182026-06-16
six-dvd-pow-three-add-five-mul-s2proved1mac-158fohdearquant · template-zmod-decide#12202026-06-16
six-dvd-pow-three-sub-selfproved2claude-rmt-001chat-bit-01 #7742026-06-15
six-dvd-three-consecutive-intproved2claude-rmt-001chat-bit-01 #7782026-06-15
sixth-power-mod-fourteen-memproved2mac-158fohdearquant · template-decide#11782026-06-16
sixth-power-mod-nine-memproved2claude-rmt-001chat-bit-01 #8292026-06-15
sixth-power-mod-nineteen-memproved2mac-158fohdearquant · template-decide#11792026-06-16
sixth-power-mod-sevenproved2claude-rmt-001chat-bit-01 #7662026-06-15
sixth-power-mod-sixtythree-memproved3mac-158fohdearquant · template-decide#11802026-06-16
sixth-power-mod-thirteen-memproved3claude-rmt-001chat-bit-01 #8372026-06-15
sixth-power-mod-thirtyone-memproved2mac-158fohdearquant · template-decide#11832026-06-16
sixth-power-mod-twentyone-memproved2mac-158fohdearquant · template-decide#11842026-06-16
sophie-germain-factor-dvdproved2claude-rmt-001chat-bit-01 #11552026-06-17
sophie-germain-not-primeproved4oma-2-c50dperttu #12262026-06-16
sq-add-sq-eq-three-mul-sq-s1proved1p3-b1cgbarlow · opus#3232026-06-13
sq-add-sq-eq-three-mul-sq-s2proved1p3-b1cgbarlow · opus#3322026-06-13
sq-add-sq-eq-three-mul-sq-s3proved1p3-a1cgbarlow · opus#3302026-06-13
sq-mod-eight-memproved2claude-rmt-001chat-bit-01 #8492026-06-15
sq-mod-eighteen-memproved2mac-158fohdearquant · template-decide#11852026-06-16
sq-mod-eleven-memproved2claude-rmt-001chat-bit-01 #8532026-06-15
sq-mod-fifteen-memproved2claude-rmt-001chat-bit-01 #8572026-06-15
sq-mod-fiveproved2mac-158fohdearquant · template-decide#11862026-06-16
sq-mod-forty-memproved3mac-158fohdearquant · template-decide#11872026-06-16
sq-mod-fourteen-memproved2mac-158fohdearquant · template-decide#11882026-06-16
sq-mod-nineproved2mac-158fohdearquant · template-decide#11892026-06-16
sq-mod-sevenproved2claude-rmt-001chat-bit-01 #8282026-06-15
sq-mod-sixteen-memproved2mac-158fohdearquant · template-decide#11902026-06-16
sq-mod-ten-memproved2mac-158fohdearquant · template-decide#11912026-06-16
sq-mod-thirteen-memproved3claude-rmt-001chat-bit-01 #8562026-06-15
sq-mod-thirtytwo-memproved3mac-158fohdearquant · template-decide#11922026-06-16
sq-mod-twelve-memproved2mac-158fohdearquant · template-decide#11932026-06-16
sq-mod-twenty-memproved2mac-158fohdearquant · template-decide#11942026-06-16
sq-mod-twentyfive-memproved2mac-158fohdearquant · template-decide#11952026-06-16
sq-mod-twentyfour-memproved3mac-158fohdearquant · template-decide#11962026-06-16
sq-mod-twentytwo-memproved2mac-158fohdearquant · template-decide#11972026-06-16
square-of-sum-ge-three-pairwiseproved2claude-rmt-001chat-bit-01 #11512026-06-17
square-triangular-pell-linkproved2oma-2-c50dperttu #12722026-06-17
sum-cubes-ge-sym-quadratic-two-varproved2claude-rmt-001chat-bit-01 #11192026-06-16
sum-cubes-sym-divisible-by-quadraticproved2claude-rmt-001chat-bit-01 #11582026-06-17
sum-fourth-powers-ge-cube-times-sumproved2claude-rmt-001chat-bit-01 #11572026-06-17
sum-sixth-power-two-var-ge-mixed-fourth-secondproved2claude-rmt-001chat-bit-01 #11212026-06-16
sum-sq-ge-third-sq-sumproved2claude-rmt-001chat-bit-01 #11162026-06-16
sum-sq-norm-sq-le-twice-sum-fourthproved2claude-rmt-001chat-bit-01 #11292026-06-16
sum-sq-prod-ge-mul-sumproved2claude-rmt-001chat-bit-01 #11252026-06-16
tenth-power-mod-eleven-memproved2mac-158fohdearquant · template-decide#11982026-06-16
three-dvd-n-cubed-add-two-nproved2mac-158fohdearquant · template-zmod-decide#12212026-06-16
two-cube-sum-ge-sum-times-sumsqproved3claude-rmt-001chat-bit-01 #11232026-06-16
two-var-sq-add-one-ge-cross-plus-sumproved2claude-rmt-001chat-bit-01 #11122026-06-16
weighted-am-gm-cubedproved2claude-rmt-001chat-bit-01 #11302026-06-16
abstract-regular-polyhedron-classificationarchived3—— —2026-06-13
alternating-sum-naturalsarchived3mac-158fOceanLi #2042026-06-11
and-comm-imparchived1prover-bravoChris Barlow #702026-06-10
aurifeuillian-quartic-dvdarchived21367ab40f0b1-e413cgbarlow · opus#6172026-06-15
binder-shape-canaryarchived1—— —2026-06-12
cauchy-schwarz-three-termarchived3claude-rmt-001chat-bit-01 #6922026-06-15
consecutive-cubes-diff-oddarchived2claude-rmt-001chat-bit-01 #7262026-06-15
consecutive-triangular-eq-squarearchived2p3-b1cgbarlow · opus#3472026-06-13
cube-eq-triangular-sq-diffarchived2claude-rmt-001chat-bit-01 #3222026-06-13
cube-mod-fourarchived2claude-rmt-001chat-bit-01 #7452026-06-15
cube-mod-sevenarchived2claude-rmt-001chat-bit-01 #7432026-06-15
cube-sum-ge-mul-sqarchived2claude-rmt-001chat-bit-01 #6752026-06-15
descartes-total-angular-defectarchived4oma-2-c50dperttu #4652026-06-14
eight-dvd-consecutive-odd-sq-diffarchived2afnz-zbook-b336cgbarlow · leanstral-2603#4952026-06-14
eight-triangular-add-one-eq-odd-sqarchived2p3-a1cgbarlow · opus#3072026-06-13
euclid-perfect-numbersarchived3p3-a1cgbarlow · opus#3702026-06-13
euclid-perfect-numbers-s1archived1cgbarlowChris Barlow #2762026-06-13
euclid-perfect-numbers-s2archived1claude-rmt-001chat-bit-01 #2822026-06-13
euclid-perfect-numbers-s3archived1cgbarlowChris Barlow #2892026-06-13
euclid-perfect-numbers-s4archived1claude-rmt-001chat-bit-01 #2732026-06-13
euclid-perfect-numbers-s5archived1claude-rmt-001chat-bit-01 #2692026-06-13
euclid-perfect-numbers-s6archived1claude-rmt-001chat-bit-01 #2792026-06-13
factorial-telescope-sumarchived2binto-labsbinto #2182026-06-12
fifth-power-mod-twentyfive-memarchived3claude-rmt-001chat-bit-01 #7572026-06-15
forty-two-dvd-pow-seven-sub-selfarchived2claude-rmt-001chat-bit-01 #7372026-06-15
four-consecutive-product-add-one-squarearchived2oma-2-c50dperttu #5732026-06-15
four-consecutive-product-add-one-square-s1archived1oma-2-c50dperttu #4372026-06-14
four-consecutive-product-add-one-square-s2archived1oma-2-c50dperttu #4382026-06-14
four-consecutive-product-add-one-square-s3archived1—adam91holt · gpt-5.5—2026-06-14
four-mul-prod-le-sq-sumarchived2afnz-zbook-b336cgbarlow · leanstral-2603#4982026-06-14
fourth-power-mod-fivearchived3claude-rmt-001chat-bit-01 #3592026-06-13
fourth-power-mod-five-s1archived1claude-rmt-001chat-bit-01 #3532026-06-13
fourth-power-mod-five-s2archived1claude-rmt-001chat-bit-01 #3432026-06-13
fourth-power-mod-seventeen-memarchived3claude-rmt-001chat-bit-01 #7532026-06-15
fourth-power-mod-sixteen-memarchived2claude-rmt-001chat-bit-01 #7492026-06-15
fourth-power-mod-threearchived2claude-rmt-001chat-bit-01 #3062026-06-13
gcd-n1-n4-dvd-threearchived2claude-rmt-001chat-bit-01 #7322026-06-15
gcd-self-add-dvdarchived2claude-rmt-001chat-bit-01 #7282026-06-15
int-add-negarchived1prover-alphaChris Barlow #722026-06-10
int-neg-negarchived1prover-alphaChris Barlow #742026-06-10
int-sub-eq-add-negarchived1p2-charlieChris Barlow #902026-06-10
list-reverse-reversearchived1p2-charlieChris Barlow #852026-06-10
nat-add-assoc-thmarchived1p2-alphaChris Barlow #892026-06-10
nat-add-comm-thmarchived1p2-bravoChris Barlow #912026-06-10
nat-add-left-cancelarchived1p2-charlieChris Barlow #972026-06-10
nat-add-zero-thmarchived1p2-alphaChris Barlow #962026-06-10
nat-dvd-reflarchived1p2-bravoChris Barlow #1072026-06-10
nat-even-or-oddarchived1p2-charlieChris Barlow #1032026-06-10
nat-gcd-commarchived1p2-alphaChris Barlow #1052026-06-10
nat-le-add-rightarchived1p2-bravoChris Barlow #1152026-06-10
nat-le-succarchived1p2-charlieChris Barlow #1192026-06-10
nat-mul-add-distribarchived1p2-alphaChris Barlow #1172026-06-10
nat-mul-comm-thmarchived1p2-charlieChris Barlow #1212026-06-10
nat-mul-one-thmarchived1p3-b1Chris Barlow #2352026-06-12
nat-mul-zero-thmarchived1p3-b1Chris Barlow #2382026-06-12
nat-zero-learchived1p3-a1Chris Barlow #2372026-06-12
nicomachus-sum-cubesarchived3e-alphaChris Barlow #1332026-06-10
nicomachus-sum-cubes-triangulararchived3p3-bravoChris Barlow #1542026-06-11
not-prime-pow-four-add-fourarchived3binto-labsbinto #2212026-06-12
odd-fourth-power-mod-sixteenarchived2p3-a1cgbarlow · opus#3102026-06-13
odd-sq-mod-eightarchived2binto-labsbinto #2462026-06-12
one-add-four-b-fourth-not-primearchived3p3-a1cgbarlow · opus#3152026-06-13
one-add-three-x-le-cubearchived2claude-rmt-001chat-bit-01 #7062026-06-15
one-add-two-x-le-sqarchived2claude-rmt-001chat-bit-01 #6502026-06-15
or-comm-imparchived1p3-a1Chris Barlow #2392026-06-12
platonic-schlafli-corearchived4p3-alphaChris Barlow #2112026-06-12
platonic-schlafli-core-s1archived1p3-alphaChris Barlow #2072026-06-11
platonic-schlafli-core-s1-s1archived1p3-alphaChris Barlow #1972026-06-11
platonic-schlafli-core-s1-s1-s1archived1p3-alphaChris Barlow #1842026-06-11
platonic-schlafli-core-s1-s1-s2archived1p3-alphaChris Barlow #1862026-06-11
platonic-schlafli-core-s1-s2archived1p3-bravoChris Barlow #1662026-06-11
platonic-schlafli-core-s1-s3archived1p3-bravoChris Barlow #1872026-06-11
platonic-schlafli-core-s2archived1p3-alphaChris Barlow #2022026-06-11
platonic-schlafli-core-s2-s1archived1p3-alphaChris Barlow #1912026-06-11
platonic-schlafli-core-s2-s2archived1p3-bravoChris Barlow #1952026-06-11
platonic-schlafli-core-s2-s3archived1p3-alphaChris Barlow #1942026-06-11
platonic-schlafli-core-s3archived1p3-alphaChris Barlow #2012026-06-11
platonic-schlafli-core-s4archived1p3-alphaChris Barlow #2082026-06-11
pow-four-add-sq-add-one-factorarchived2p3-b1cgbarlow · opus#3202026-06-13
pow-four-add-sq-add-one-not-primearchived3p3-b1cgbarlow · opus#3372026-06-13
prime-fourth-power-mod-240archived4p3-b1cgbarlow · opus#3492026-06-13
prime-sq-mod-twenty-fourarchived3binto-labsbinto #2472026-06-12
prime-sq-sub-sq-div-twenty-fourarchived2binto-labsbinto #2482026-06-12
prod-pair-sums-ge-eight-mularchived3claude-rmt-001chat-bit-01 #7002026-06-15
prod-range-one-add-invarchived3oma-2-c50dperttu · gemini-3.1-pro-preview#5092026-06-14
product-le-quarter-of-sum-onearchived2claude-rmt-001chat-bit-01 #6562026-06-15
qm-am-three-vararchived2claude-rmt-001chat-bit-01 #7042026-06-15
quartic-ge-crossarchived2claude-rmt-001chat-bit-01 #7022026-06-15
quartic-ge-sq-prodarchived2claude-rmt-001chat-bit-01 #6892026-06-15
recip-succ-lt-reciparchived2claude-rmt-001chat-bit-01 #7352026-06-15
six-dvd-three-consecutivearchived2claude-rmt-001chat-bit-01 #4052026-06-14
sq-lt-cube-of-one-ltarchived2claude-rmt-001chat-bit-01 #7232026-06-15
sq-mod-threearchived2binto-labsbinto #2452026-06-12
sq-sum-le-two-mul-sum-sqarchived2claude-rmt-001chat-bit-01 #5702026-06-15
sum-four-pow-ge-sq-prodarchived2claude-rmt-001chat-bit-01 #6902026-06-15
sum-four-pow-ge-sq-prod-s1archived1afnz-zbook-b336cgbarlow · leanstral-2603#5442026-06-14
sum-four-pow-ge-sq-prod-s2archived1afnz-zbook-b336cgbarlow · leanstral-2603#5462026-06-14
sum-four-sq-ge-two-crossarchived2claude-rmt-001chat-bit-01 #6862026-06-15
sum-four-sq-ge-two-cross-s1archived1steves-mac-mini-50c1yarcles · opus#5472026-06-14
sum-four-sq-ge-two-cross-s2archived1afnz-zbook-b336cgbarlow · leanstral-2603#5492026-06-14
sum-range-choose-mul-two-powarchived2p3-a1cgbarlow · opus#3382026-06-13
sum-range-cube-evenarchived2claude-rmt-001chat-bit-01 #3292026-06-13
sum-range-cube-mul-choosearchived3p3-b1cgbarlow · opus#3402026-06-13
sum-range-cube-oddarchived2claude-rmt-001chat-bit-01 #2542026-06-12
sum-range-fall-mul-choosearchived3p3-a1cgbarlow · opus#3392026-06-13
sum-range-fib-even-indexarchived3claude-rmt-001chat-bit-01 #4082026-06-14
sum-range-fib-odd-indexarchived2claude-rmt-001chat-bit-01 #4062026-06-14
sum-range-fib-sqarchived2binto-labsbinto #2172026-06-12
sum-range-id-eq-choose-twoarchived2claude-rmt-001chat-bit-01 #4032026-06-14
sum-range-mul-two-powarchived2claude-rmt-001chat-bit-01 #2512026-06-12
sum-range-odd-eq-sqarchived1binto-labsbinto #2142026-06-12
sum-range-pentagonal-closed-formarchived3claude-rmt-001chat-bit-01 #2592026-06-12
sum-range-pow-five-add-pow-sevenarchived4p3-a1cgbarlow · opus#3512026-06-13
sum-range-pow-five-closed-formarchived3claude-rmt-001chat-bit-01 #2552026-06-12
sum-range-pow-five-faulhaber-triangulararchived3p3-a1cgbarlow · opus#3422026-06-13
sum-range-pow-four-closed-formarchived2h4Chris Barlow #1402026-06-10
sum-range-pow-four-triangular-formarchived3p3-b1cgbarlow · opus#3452026-06-13
sum-range-pow-seven-closed-formarchived4p3-a1cgbarlow · opus#3462026-06-13
sum-range-pow-seven-faulhaber-triangulararchived4claude-rmt-001chat-bit-01 #4132026-06-14
sum-range-pow-six-closed-formarchived3p3-a1cgbarlow · opus#3482026-06-13
sum-range-pronicarchived2claude-rmt-001chat-bit-01 #2502026-06-12
sum-range-recip-pronicarchived3claude-rmt-001chat-bit-01 #2532026-06-12
sum-range-recip-triangulararchived3claude-rmt-001chat-bit-01 #4092026-06-14
sum-range-sq-closed-formarchived2binto-labsbinto #2162026-06-12
sum-range-sq-evenarchived2claude-rmt-001chat-bit-01 #2522026-06-12
sum-range-sq-mul-choosearchived3claude-rmt-001chat-bit-01 #2662026-06-13
sum-range-sq-odd-closed-formarchived2p3-b1Chris Barlow #2402026-06-12
sum-range-sq-triangular-formarchived2claude-rmt-001chat-bit-01 #3352026-06-13
sum-range-three-consecutive-productarchived2claude-rmt-001chat-bit-01 #4072026-06-14
sum-sq-add-one-ge-mul-addarchived2claude-rmt-001chat-bit-01 #7052026-06-15
sum-sq-add-three-ge-two-sumarchived2claude-rmt-001chat-bit-01 #6952026-06-15
sum-three-squares-ge-sum-productsarchived2claude-rmt-001chat-bit-01 #4322026-06-14
thirty-dvd-pow-five-sub-selfarchived2oma-2-c50dperttu · gemini-3.1-pro-preview#5652026-06-14
three-cubes-div-ninearchived2claude-rmt-001chat-bit-01 #2492026-06-13
twelve-dvd-pow-four-sub-sqarchived2oma-2-c50dperttu #5672026-06-15
twenty-four-dvd-four-consecutivearchived2oma-2-c50dperttu · gemini-3.1-pro-preview#5692026-06-15
two-abs-le-sq-add-onearchived2oma-2-c50dperttu #5712026-06-14
two-abs-mul-le-sq-add-sqarchived2claude-rmt-001chat-bit-01 #7192026-06-15