Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Nov 4, 2025

• Erdős Problem 283 (#1172)

  Show description for 4b3335d
  

  mo271

  and

  Paul-Lez

  authored
  4b3335d

  Copy full SHA for 4b3335d

• Erdős Problem 67: The Erdős discrepancy problem (#1173)

  Show description for 3400da0
  

  mo271

  and

  Paul-Lez

  authored
  3400da0

  Copy full SHA for 3400da0

• fix some missing namespaces and correct docstrings (#1171)

  mo271

  authored
  fb2990c

  Copy full SHA for fb2990c

Commits on Nov 3, 2025

• fix distinctDistances (#1169)

  Show description for ea5115a
  mo271

  authored
  ea5115a

  Copy full SHA for ea5115a

Commits on Nov 2, 2025

• Erdős Problem 14 (#1148)

  Show description for 97c766c
  

  edwag

  and

  mo271

  authored
  97c766c

  Copy full SHA for 97c766c

• Add Erdős Problem 1059 (#1130)

  Show description for e641540
  

  edwag

  and

  callesonne

  authored
  e641540

  Copy full SHA for e641540

Commits on Oct 29, 2025

• fix: `erdos_273.variants.three` is solved (#1166)

  smmercuri

  authored
  9436b71

  Copy full SHA for 9436b71

• fix: remove claims about squares being Sidon in `329.lean` (#1165)

  Show description for f9e16a9
  smmercuri

  authored
  f9e16a9

  Copy full SHA for f9e16a9

• fix: nat division in `erdos_357.variants.infinite_set_sum` (#1160)

  smmercuri

  authored
  25e9df2

  Copy full SHA for 25e9df2

• fix: `erdos_307_coprime` (#1159)

  Show description for 4cc70da
  smmercuri

  authored
  4cc70da

  Copy full SHA for 4cc70da

• fix: missing quantification in `944.lean` (#1156)

  Show description for e51d5ff
  smmercuri

  authored
  e51d5ff

  Copy full SHA for e51d5ff

• fix: `erdos_128` should use induced subgraphs (#1151)

  Show description for 0bc24ad
  smmercuri

  authored
  0bc24ad

  Copy full SHA for 0bc24ad

• fix: add missing composite conditions in `AgohGiuga.lean` (#1164)

  Show description for f3cfdef
  smmercuri

  authored
  f3cfdef

  Copy full SHA for f3cfdef

• conjectures from OEIS 034693 (#1150)

  Show description for a63533f
  

  smmercuri

  and

  mo271

  authored
  a63533f

  Copy full SHA for a63533f

Commits on Oct 28, 2025

• fix: `exists_semiring_unique_left_right_maximal_ne` (#1163)

  Show description for 217e2fc
  smmercuri

  authored
  217e2fc

  Copy full SHA for 217e2fc

• fix: quantification in `Erdos672With` (#1162)

  Show description for 5fc6cc1
  smmercuri

  authored
  5fc6cc1

  Copy full SHA for 5fc6cc1

• fix: positivity in `erdos_728` (#1161)

  Show description for 3193948
  smmercuri

  authored
  3193948

  Copy full SHA for 3193948

• fix: add positivity condition in `erdos_306.variant.integer_three_primes` (#1158)

  Show description for 0d8dfed
  smmercuri

  authored
  0d8dfed

  Copy full SHA for 0d8dfed

• fix: `n > 0` required in `erdos_942` (#1157)

  Show description for 4675109
  smmercuri

  authored
  4675109

  Copy full SHA for 4675109

• fix: `erdos_828.variants.phi_dvd_self_iff_pow2_pow3` (#1155)

  Show description for f25c23a
  smmercuri

  authored
  f25c23a

  Copy full SHA for f25c23a

• fix: missing positivity condition in `erdos_1003.variants.eps87` (#1154)

  Show description for 79ba9c6
  smmercuri

  authored
  79ba9c6

  Copy full SHA for 79ba9c6

• fix: missing positivity condition in `erdos_44.empty_start` (#1153)

  Show description for 9fbb9e7
  smmercuri

  authored
  9fbb9e7

  Copy full SHA for 9fbb9e7

• fix: `erdos_366` should exclude `n = 0` (#1152)

  Show description for 5ed3a28
  smmercuri

  authored
  5ed3a28

  Copy full SHA for 5ed3a28

Commits on Oct 27, 2025

• Fix namespaces in `BusyBeaver.lean` (#1149)

  Show description for 7063010
  Paul-Lez

  authored
  7063010

  Copy full SHA for 7063010

Commits on Oct 24, 2025

• Erdős Problem 89 (#657)

  Show description for afc605b
  

  3 peopleauthored
  afc605b

  Copy full SHA for afc605b

• OEIS 228828 (#1145)

  Show description for f204451
  

  mo271

  and

  callesonne

  authored
  f204451

  Copy full SHA for f204451

• Added Erdos 1056. (#1133)

  Show description for 1961c3f
  

  zond

  and

  mo271

  authored
  1961c3f

  Copy full SHA for 1961c3f

Commits on Oct 23, 2025

• Kummer-Vandiver conjecture (#297)

  Show description for 7ff1f85
  

  4 peopleauthored
  7ff1f85

  Copy full SHA for 7ff1f85

• Erdős 707: update solution status and add `0<n` assumption (#1138)

  Show description for 070da0e
  

  4 peopleauthored
  070da0e

  Copy full SHA for 070da0e

• Erdős 786: fix consecutivePrimes (#1143)

  mo271

  authored
  3192bdc

  Copy full SHA for 3192bdc

• fix overwrite_index: importModules changes (#1142)

  Show description for 4b01fd3
  mo271

  authored
  4b01fd3

  Copy full SHA for 4b01fd3

• Add infinitude of Mersenne primes (#1136)

  edwag

  authored
  3358720

  Copy full SHA for 3358720

• fixes after bump to `v4.22.0` (#1141)

  mo271

  authored
  f11df4d

  Copy full SHA for f11df4d

Commits on Oct 22, 2025

• bump toolchain and Mathlib to v4.22.0 (#603)

  mo271

  authored
  952798f

  Copy full SHA for 952798f

• bump toolchain and Mathlib to v4.21.0 (#602)

  Show description for 044be64
  

  3 peopleauthored
  044be64

  Copy full SHA for 044be64

Pagination

Previous

Next