{"total":327,"submissions_open":true,"items":[{"slug":"artinprimitiverootsconjecture-artin-primitive-roots-parts-i","display_title":"Artin Primitive Roots Conjecture - part i","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Artin Primitive Roots Conjecture","qualifier":"part i"},"title":"ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i","statement":"∀ (a : ℤ), ¬IsSquare a → a ≠ -1 → ∃ x > 0, (ArtinPrimitiveRootsConjecture.S a).HasDensity x {p | Nat.Prime p}","summary":"**Artin's Conjecture on Primitive Roots**, first half.\nLet $a$ be an integer that is not a square number and not $−1$. Then the set $S(a)$\nof primes $p$ such that $a$ is a primitive root modulo $p$ has a positive asymptotic\ndensity inside the set of primes. In particular, $S(a)$ is infinite.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-parts-i-5894b7601f82bbd7963740be44f33d00-problem","reward_target_id":"fc-target:ArtinPrimitiveRootsConjecture.artin_primitive_roots.parts.i","tasks":[{"task_id":"fc-v2-parts-i-4747654486a672d04029106d-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:4619e86bd446c1becd74c13e544fe75880f79c0492d735149fb851a8fe8355df","attempts":0},{"task_id":"fc-v2-parts-i-d39af85683916954dbfdb85e-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:b4799e4a029629f8b048aef41a76ce3bf8a1a11422e184c02bea3ea0e2478d40","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"borsuk-borsuk-conjecture-four","display_title":"Borsuk Conjecture - four","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Borsuk Conjecture","qualifier":"four"},"title":"Borsuk.borsuk_conjecture.four","statement":"Borsuk.BorsukConjecture 4","summary":"**Borsuk's conjecture** in dimension $4$, the smallest open case. ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[52],"is_open":true,"problem_id":"fc-33b3c405-borsuk-conjecture-four-0a98f6bc95f215bcf86e723ea7e14500-problem","reward_target_id":"fc-target:Borsuk.borsuk_conjecture.four","tasks":[{"task_id":"fc-v2-borsuk-conjecture-four-c5ec39a2e30c2f7226decfbb-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:b13b9bd4d94e835f6c6756030f517d9609efcf61be17f6054ef41b8ec669e698","attempts":0},{"task_id":"fc-v2-borsuk-conjecture-four-2603ae47c01869b59512f14f-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:307fb0a48690d977ab0ae0b2a1c12354dcf86a0e87e6829528c3e2475775f590","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"brocard-brocard-conjecture","display_title":"Brocard Conjecture","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Brocard Conjecture","qualifier":null},"title":"Brocard.brocard_conjecture","statement":"∀ (n : ℕ),\n  1 ≤ n → 4 ≤ (Finset.filter Nat.Prime (Finset.Ioo (Nat.nth Nat.Prime n ^ 2) (Nat.nth Nat.Prime (n + 1) ^ 2))).card","summary":"**Brocard's Conjecture**\nFor every `n ≥ 2`, between the squares of the `n`-th and `(n+1)`-th primes,\nthere are at least four prime numbers.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-brocard-brocard-conjecture-a622659ed8aca821a722b3046a6967b2-problem","reward_target_id":"fc-target:Brocard.brocard_conjecture","tasks":[{"task_id":"fc-v2-brocard-brocard-conjecture-bad8d38c7152fb324800c317-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:f85d6f078fbafebba06fe7046daaf7e85edee6fa202805bdc6c1b3282f2bacd4","attempts":0},{"task_id":"fc-v2-brocard-brocard-conjecture-d612eddd45660c17c5082fcd-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:283fddc1f137edcb0e744c764774155ac5992a19b86a0dc218c3f22a4254471c","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"bunyakovsky-bunyakovsky-conjecture","display_title":"Bunyakovsky","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Bunyakovsky","qualifier":null},"title":"Bunyakovsky.bunyakovsky_conjecture","statement":"∀ (f : Polynomial ℤ),\n  BunyakovskyCondition f ∧ SchinzelCondition {f} → Infinite ↑{n | Nat.Prime (Polynomial.eval (↑n) f).natAbs}","summary":"**Bunyakovsky conjecture**\nIf a polynomial $f$ over integers satisfies both Schinzel and Bunyakovsky conditions,\nthere exist infinitely many natural numbers $m$ such that $f(m)$ is prime.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-bunyakovsky-bunyakovsky-conjecture-a98131fb015631153cf6634d3192da0a-problem","reward_target_id":"fc-target:Bunyakovsky.bunyakovsky_conjecture","tasks":[{"task_id":"fc-v2-bunyakovsky-bunyakovsky-conjecture-495d8670e29bf5ff57f0d793-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:f9cdc4f4e4f3138a7bd972423903f9e22d7172275efcf3ee1bac97b88ba70723","attempts":0},{"task_id":"fc-v2-bunyakovsky-bunyakovsky-conjecture-d4d8704e2addca422ba02457-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:0a4001f3c05aac250d1601ab89f768b54c6d962ffb15da18ed324d4ed95672a4","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"carmichaeltotient-charmichaeltotient","display_title":"Carmichael Totient - charmichael Totient","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Carmichael Totient","qualifier":"charmichael Totient"},"title":"CarmichaelTotient.charmichaelTotient","statement":"∀ ⦃n : ℕ⦄, 0 < n → CarmichaelTotient.CarmichaelTotientFor n","summary":"*Carmichael's totient function conjecture*: For every positive natural number $n$,\nthere exists a natural number $m$ with $m ≠ n$, such that $φ(n) = φ(m)$. ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-carmichaeltotient-charmichaeltotient-60fac550eaedb6870254a9017e51a7ef-problem","reward_target_id":"fc-target:CarmichaelTotient.charmichaelTotient","tasks":[{"task_id":"fc-v2-carmichaeltotient-charmichaeltotient-cae8e89f6c888ed860b526e4-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:1cb7f321b3a7d88f005f6649a76744e7fe0ee5b0d10a91fde08865c8163f9195","attempts":0},{"task_id":"fc-v2-carmichaeltotient-charmichaeltotient-3fcc21388d36e5dddf7818a9-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:ab8baa032fa5ef7f85ba6b8f7268bab5d44d3e283d6af43ebff3bef4d7f2b5a7","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"classnumberproblem-class-number-problem","display_title":"Class Number Problem","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Class Number Problem","qualifier":null},"title":"ClassNumberProblem.class_number_problem","statement":"{d | Squarefree d ∧ d > 1 ∧ ClassNumberProblem.IsClassNumberOne d}.Infinite","summary":"There are infinitely many real quadratic fields `ℚ(√d)` with class number one,\nwhere `d > 1` is a squarefree integer.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-classnumberproblem-class-number-problem-54b84e3c8e67b8906e18557149f43af0-problem","reward_target_id":"fc-target:ClassNumberProblem.class_number_problem","tasks":[{"task_id":"fc-v2-classnumberproblem-class-number-problem-8829b1f898f6541d3a2b7305-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:9110cbec5bbdd577fe0274a4d829dd8d98311eb4c4233993a83e414b1e374316","attempts":0},{"task_id":"fc-v2-classnumberproblem-class-number-problem-1e9408c8861d20ef244dc7ed-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:3a281871f33bcbd46ab0ad3dfd4b114c1969ce75ccbb2177a48679948b3e522f","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"dickson-dickson-conjecture","display_title":"Dickson","title_parts":{"collection":"wikipedia","collection_label":"Wikipedia","reference":"Dickson","qualifier":null},"title":"Dickson.dickson_conjecture","statement":"∀ (fs : Finset (Polynomial ℤ)),\n  (∀ f ∈ fs, f.degree = 1 ∧ BunyakovskyCondition f) →\n    SchinzelCondition fs → Infinite ↑{n | ∀ f ∈ fs, Nat.Prime (Polynomial.eval (↑n) f).natAbs}","summary":"**Dickson's conjecture**\nIf a finite set of linear integer forms $f_i(n) = a_i n+b_i$ satisfies Schinzel condition,\nthere exist infinitely many natural numbers $m$ such that $f_i(m)$ are primes for all $i$.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-dickson-dickson-conjecture-cb354232b775422582d7101db209b602-problem","reward_target_id":"fc-target:Dickson.dickson_conjecture","tasks":[{"task_id":"fc-v2-dickson-dickson-conjecture-8d0fad8afc24b80bb153877f-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:454a80b41ade5aef80a0b6f7f8f7448c4a322489bda0f17ecfb92b275dbd3c6d","attempts":0},{"task_id":"fc-v2-dickson-dickson-conjecture-253b4fbc1634bfc8451d8649-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:25fb313cc56f20b2cc4d99062c23f22324e618e3c7b6f0adc95118e0d51ef7dd","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"erdos10-erdos-10","display_title":"Erdős problem 10","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"10","qualifier":null},"title":"Erdos10.erdos_10","statement":"True ↔ ∃ k, Erdos10.sumPrimeAndTwoPows k = Set.univ \\ {0, 1}","summary":"Is there some $k$ such that every integer is the sum of a prime and at most $k$\npowers of $2$?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[5,11],"is_open":true,"problem_id":"fc-33b3c405-erdos10-erdos-10-d396e57fbf40722a4d1e74c16dda1ecb-problem","reward_target_id":"fc-target:Erdos10.erdos_10","tasks":[{"task_id":"fc-v2-erdos10-erdos-10-093efee199e3118d7c812e2a-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:3f52c15449a671f2c6bfc082b7e01ba5c6156147787fb60562497c87dce060a0","attempts":0},{"task_id":"fc-v2-erdos10-erdos-10-abdccd90fbce1064f5d6e4dc-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:f13a3ae2a50c611afab2229a8097c0050e5ed92aa5cebcdaa14eac01e33bc7b6","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-08T06:03:00Z","solved_at":null,"attempts":0},{"slug":"erdos100-erdos-100","display_title":"Erdős problem 100","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"100","qualifier":null},"title":"Erdos100.erdos_100","statement":"True ↔\n  ∃ C > 0,\n    ∀ᶠ (n : ℕ) in Filter.atTop,\n      ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑n","summary":"Is the diameter of $A$ at least $Cn$ for some constant $C > 0$? ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[52],"is_open":true,"problem_id":"fc-33b3c405-erdos100-erdos-100-117033149143aeffc2066b9502a0abb2-problem","reward_target_id":"fc-target:Erdos100.erdos_100","tasks":[{"task_id":"fc-v2-erdos100-erdos-100-095be19d890f587b8a3648c8-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:bc7ee186ac46080012c3403a9e230499155cd2082da275190ca55a4048908f63","attempts":0},{"task_id":"fc-v2-erdos100-erdos-100-483fd180d91aeb4a44f24fc4-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:ddf3e7b34ee541e16819f4e045496eac6fdd933b596815e87424d64abd776911","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-05T16:07:00Z","solved_at":null,"attempts":0},{"slug":"erdos1003-erdos-1003","display_title":"Erdős problem 1003","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1003","qualifier":null},"title":"Erdos1003.erdos_1003","statement":"True ↔ {n | n.totient = (n + 1).totient}.Infinite","summary":"Are there infinitely many solutions to $\\phi(n) = \\phi(n+1)$, where $\\phi$ is the Euler totient\nfunction?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-erdos1003-erdos-1003-5233323920ab11189562723ba8b95de1-problem","reward_target_id":"fc-target:Erdos1003.erdos_1003","tasks":[{"task_id":"fc-v2-erdos1003-erdos-1003-ca6862d8b79e6409eaa9d6ed-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:19321a80efcbddb4cdd4ef660ea0a9fb60a0839f21fd9522750da13261317466","attempts":0},{"task_id":"fc-v2-erdos1003-erdos-1003-0a9b27fd57a7d9a3165b749e-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:4f768a1964915505b602bb7667aa95e5b58d314f637980dcab7f30b427822247","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-05T16:07:00Z","solved_at":null,"attempts":1},{"slug":"erdos102-erdos-102","display_title":"Erdős problem 102","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"102","qualifier":null},"title":"Erdos102.erdos_102","statement":"∀ c > 0, ∀ (M : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑M ≤ Erdos102.h c n","summary":"Let $c > 0$ and let $h_c(n)$ be such that for any $n$ points in $\\mathbb{R}^2$ with at least\n$cn^2$ lines that each contain more than three of the points, some line contains $h_c(n)$ of\nthe points. Is it true that, for fixed $c > 0$, $h_c(n) \\to \\infty$?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[52],"is_open":true,"problem_id":"fc-33b3c405-erdos102-erdos-102-60e60185e29ed021989b6dfc1ab70e1b-problem","reward_target_id":"fc-target:Erdos102.erdos_102","tasks":[{"task_id":"fc-v2-erdos102-erdos-102-b12433b49d2d2a7aeed8f85f-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:7c7bf4606d130bb9915a50adc7d74d8cef5df3f373eadd5c51bd6c6fae3d1d74","attempts":0},{"task_id":"fc-v2-erdos102-erdos-102-093218bda75a2bb746a9f7fe-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:ab98f3d98a5c83cd0c5a262bc6a416c96e936fae79a9cb1c3cb26ce73a44f6fd","attempts":0}],"bounty":{"amount_rao":6016205196857,"amount_usd":"2522.51","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-11-06T00:00:00Z","solved_at":null,"attempts":0},{"slug":"erdos103-erdos-103","display_title":"Erdős problem 103","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"103","qualifier":null},"title":"Erdos103.erdos_103","statement":"Filter.Tendsto Erdos103.h Filter.atTop (nhds ⊤)","summary":"Let $h(n)$ count the number of incongruent sets of $n$ points in $\\mathbb{R}^2$ which minimise\nthe diameter subject to the constraint that $d(x,y)\\geq 1$ for all points $x\\neq y$. Is it true\nthat $h(n)\\to \\infty$?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[52],"is_open":true,"problem_id":"fc-33b3c405-erdos103-erdos-103-2443e0bc0ae775afbbda4ea536ff3524-problem","reward_target_id":"fc-target:Erdos103.erdos_103","tasks":[{"task_id":"fc-v2-erdos103-erdos-103-ee78d2696e0e757f165095a6-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:b75223fd8a2c12132c70ee8a53319bd983f18b87670c242202e9a3fd0eaaafdb","attempts":0},{"task_id":"fc-v2-erdos103-erdos-103-65b0783f901801b2d7bcfe36-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:3e693db16cf70502e4bbcba69845a695371c562838064ee0b9862793b248372e","attempts":0}],"bounty":{"amount_rao":6016205196857,"amount_usd":"2522.51","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-11-06T00:00:00Z","solved_at":null,"attempts":0},{"slug":"erdos104-erdos-104","display_title":"Erdős problem 104","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"104","qualifier":null},"title":"Erdos104.erdos_104","statement":"(fun n => ↑(Erdos104.maxUnitCircleCount n)) =o[Filter.atTop] fun n => ↑n ^ 2","summary":"Given $n$ points in $\\mathbb{R}^2$ the number of distinct unit circles containing at least three points is $o(n^2)$.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[52],"is_open":true,"problem_id":"fc-33b3c405-erdos104-erdos-104-84832f9e9f226e6c5acad3672216b4cd-problem","reward_target_id":"fc-target:Erdos104.erdos_104","tasks":[{"task_id":"fc-v2-erdos104-erdos-104-7e06efdabca5b60fd20d9369-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:62d4e9cfb780505834c18efdff862ee26d54c4033b0e65176ab6e1d356a946f5","attempts":0},{"task_id":"fc-v2-erdos104-erdos-104-8295888be975a7ed11a2feb8-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:8302c872885ae5e64193aa741e206b5ab6266b866cca4db46d2b71dbad3b5b06","attempts":0}],"bounty":{"amount_rao":6016205196857,"amount_usd":"2522.51","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-11-06T00:00:00Z","solved_at":null,"attempts":0},{"slug":"erdos1049-erdos-1049","display_title":"Erdős problem 1049","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1049","qualifier":null},"title":"Erdos1049.erdos_1049","statement":"True ↔ ∀ t > 1, Irrational (∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1))","summary":"Let $t>1$ be a rational number. Is\n$\\sum_{n=1}^\\infty\\frac{1}{t^n-1}=\\sum_{n=1}^\\infty \\frac{\\tau(n)}{t^n}$ irrational, where\n$\\tau(n)$ counts the divisors of $n$?\n\nA conjecture of Chowla.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-erdos1049-erdos-1049-a8a9376d8d273c074dcda0d4cbbca56d-problem","reward_target_id":"fc-target:Erdos1049.erdos_1049","tasks":[{"task_id":"fc-v2-erdos1049-erdos-1049-113d6d510a3b1cca19a554dc-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:597f76925827a60542999e2c24a92920a73c66f976a1faf907ad20cf11eb9cd7","attempts":0},{"task_id":"fc-v2-erdos1049-erdos-1049-206b5928989e8f6e97fbb53b-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:56a01e7c35b14080996cf86d9d198206f869185d81ced7e1cbe8b3f1c44b1eb1","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-05T16:07:00Z","solved_at":null,"attempts":1},{"slug":"erdos1056-erdos-1056","display_title":"Erdős problem 1056","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1056","qualifier":null},"title":"Erdos1056.erdos_1056","statement":"True ↔\n  ∀ k ≥ 2,\n    ∃ p, ∃ (_ : Nat.Prime p), ∃ boundaries, ∃ (_ : StrictMono boundaries), Erdos1056.AllModProdEqualsOne p boundaries","summary":"Let $k ≥ 2$. Does there exist a prime $p$ and consecutive intervals $I_0,\\dots,I_k$\nsuch that $\\prod\\limits_{n{\\in}I_i}n \\equiv 1 \\mod n$ for all $1 \\le i \\le k$?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-erdos1056-erdos-1056-a43f0f4b25104af32f46463825d083e3-problem","reward_target_id":"fc-target:Erdos1056.erdos_1056","tasks":[{"task_id":"fc-v2-erdos1056-erdos-1056-4743f1ccd9bd4738e94491af-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:d0543f331e6862616623408f027ff0294f8659eb423b7c3cd2fa24b31a7b0de4","attempts":0},{"task_id":"fc-v2-erdos1056-erdos-1056-9a16a71c2bff62d52ea52bf6-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:15b16a52b79e3f75cf8ecdf1c0682fb75df64f6728dd9e0456002c151d72dc11","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-08T06:03:00Z","solved_at":null,"attempts":0},{"slug":"erdos1057-erdos-1057","display_title":"Erdős problem 1057","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1057","qualifier":null},"title":"Erdos1057.erdos_1057","statement":"True ↔ Filter.Tendsto (fun x => Real.log (Erdos1057.carmichaelCounting x) / Real.log x) Filter.atTop (nhds 1)","summary":"Is it true that $C(x)=x^{1-o(1)}$?\n\nThis is discussed in problem A13 of Guy's collection [Gu04].\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-erdos1057-erdos-1057-491cd1752259ffb23d00c3021891d151-problem","reward_target_id":"fc-target:Erdos1057.erdos_1057","tasks":[{"task_id":"fc-v2-erdos1057-erdos-1057-d6b741cdf13f9b7c3980899b-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:7a8488ac1ed343114190237377cd8c0e9bd5e3fdb70a9ca1f3a266e1daa6e1ae","attempts":0},{"task_id":"fc-v2-erdos1057-erdos-1057-10933a47619cf0c79fc816a9-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:40678d0910ec38031fca300cb6db016038a5cd77b0443dfde37410a3f1e90ed3","attempts":0}],"bounty":{"amount_rao":null,"amount_usd":null,"policy_version":"linear-age-v3-chat-logs","available":false,"reason":"ALREADY_SOLVED","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"solved","accepting_submissions":false,"added_at":"2026-08-25T00:17:00Z","solved_at":"2026-10-12T19:07:47.385670Z","attempts":1},{"slug":"erdos1060-erdos-1060-parts-ii","display_title":"Erdős problem 1060 - part ii","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1060","qualifier":"part ii"},"title":"Erdos1060.erdos_1060.parts.ii","statement":"∃ C,\n  (fun n => ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card) =O[Filter.atTop] fun n => Real.log ↑n ^ C","summary":"Part (ii) of Erdős Problem 1060: bound on the number of $k \\le n$ with $k \\sigma_1(k) = n$. ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-parts-ii-13443838f9167a1ad0692f031254c9f4-problem","reward_target_id":"fc-target:Erdos1060.erdos_1060.parts.ii","tasks":[{"task_id":"fc-v2-parts-ii-74f0ee48481a220c9ce887f3-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:e46fa4a80e17feab225a4f0f8ec2d385d83973f5ebbfb618f4b54b90b76236d9","attempts":0},{"task_id":"fc-v2-parts-ii-3a9ac8dabb835be38e0ebeeb-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:50e615012c41d56379398ba60dcad022d2a3fff15b762a2786abfe9c91f0c0b9","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-05T16:07:00Z","solved_at":null,"attempts":0},{"slug":"erdos1062-erdos-1062-parts-ii","display_title":"Erdős problem 1062 - part ii","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1062","qualifier":"part ii"},"title":"Erdos1062.erdos_1062.parts.ii","statement":"(∃ l, Filter.Tendsto (fun n => ↑(Erdos1062.f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ True","summary":"Erdős asked whether the limiting density `f n / n` exists and, if so, whether it is\nirrational. ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-parts-ii-c9250f48d3aae5a5c4b8da4653c077a5-problem","reward_target_id":"fc-target:Erdos1062.erdos_1062.parts.ii","tasks":[{"task_id":"fc-v2-parts-ii-ca03ba84817dff1342d8cb9e-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:34e80d11573bae915f50effde33736795a5dfa342ab0008cd94f877c4d61df60","attempts":0},{"task_id":"fc-v2-parts-ii-fec9c9f260cac324da2d696c-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:403f2478bc6d84341e23e782f14535f9ff593c371eeaea4dd4a898f30e1e2aaf","attempts":0}],"bounty":{"amount_rao":null,"amount_usd":null,"policy_version":"linear-age-v3-chat-logs","available":false,"reason":"ALREADY_SOLVED","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"solved","accepting_submissions":false,"added_at":"2026-09-08T06:03:00Z","solved_at":"2026-09-22T01:42:30.280362Z","attempts":1},{"slug":"erdos1068-erdos-1068","display_title":"Erdős problem 1068","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1068","qualifier":null},"title":"Erdos1068.erdos_1068","statement":"True ↔\n  ∀ (V : Type) (G : SimpleGraph V),\n    G.chromaticCardinal = Cardinal.aleph 1 → ∃ s, s.Countable ∧ (SimpleGraph.induce s G).InfinitelyConnected","summary":"Does every graph with chromatic number $\\aleph_1$ contain a countable subgraph which is\ninfinitely connected?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[5],"is_open":true,"problem_id":"fc-33b3c405-erdos1068-erdos-1068-a6fe72264a9c232b7931be5f3016efa3-problem","reward_target_id":"fc-target:Erdos1068.erdos_1068","tasks":[{"task_id":"fc-v2-erdos1068-erdos-1068-61390c258ade846781ec3a2a-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:1fa870353e76ce6360d69f48165e6d14e7c606571a03d69cb10df88671b6ee91","attempts":1},{"task_id":"fc-v2-erdos1068-erdos-1068-00124f567f171d576b85e4fe-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:be001630b8012cec34322d872e28f7455a7597bb4aa0303defc7477eaa37356e","attempts":1}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"in_review","accepting_submissions":true,"added_at":"2026-08-25T00:17:00Z","solved_at":null,"attempts":2},{"slug":"erdos107-erdos-107","display_title":"Erdős problem 107","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"107","qualifier":null},"title":"Erdos107.erdos_107","statement":"True ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1","summary":"Let $f(n)$ be minimal such that any $f(n)$ points in $ℝ^2$, no three on a line,\ncontain $n$ points which form the vertices of a convex $n$-gon.\nProve that $f(n) = 2^{n-2} + 1$.\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[52],"is_open":true,"problem_id":"fc-33b3c405-erdos107-erdos-107-2e9cddce73ae9acc19280cc0ef20eb68-problem","reward_target_id":"fc-target:Erdos107.erdos_107","tasks":[{"task_id":"fc-v2-erdos107-erdos-107-5e8746ecd04f4a99466608a8-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:f5e417eecfa784ec412667ae4ac42593e5075b60eb00db946e0485a1c7137b98","attempts":0},{"task_id":"fc-v2-erdos107-erdos-107-d8d2a601b547e460a2a6b1ec-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:73c3b47946d17553a69b3d11cfed98bc54732f9860af79e8be945a61e195c45f","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-21T20:46:00Z","solved_at":null,"attempts":0},{"slug":"erdos1072-erdos-1072-parts-i","display_title":"Erdős problem 1072 - part i","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1072","qualifier":"part i"},"title":"Erdos1072.erdos_1072.parts.i","statement":"True ↔ {p | Nat.Prime p ∧ Erdos1072.f p = p - 1}.Infinite","summary":"Is it true that there are infinitely many $p$ for which $f(p) = p − 1$? ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-parts-i-ba44cfd828532ad8cf0a4a7aae0f87fd-problem","reward_target_id":"fc-target:Erdos1072.erdos_1072.parts.i","tasks":[{"task_id":"fc-v2-parts-i-5b086664dcebd268a95494f4-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:0e4a56861d997befb6dc8032f902eebbf05da9665968f8f453aa6eb3a6861b67","attempts":0},{"task_id":"fc-v2-parts-i-59e67aad9ed74bf0c9fa9751-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:a98affeeebe5908fae2af47a49d8462c61877156b4f02296a87dbeb609f0d571","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-05T16:07:00Z","solved_at":null,"attempts":0},{"slug":"erdos1072-erdos-1072-parts-ii","display_title":"Erdős problem 1072 - part ii","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1072","qualifier":"part ii"},"title":"Erdos1072.erdos_1072.parts.ii","statement":"True ↔\n  ∃ P ⊆ {p | Nat.Prime p},\n    P.HasDensity 1 {p | Nat.Prime p} ∧\n      Filter.Tendsto (fun p => ↑(Erdos1072.f p) / ↑p) (Filter.atTop ⊓ Filter.principal P) (nhds 0)","summary":"Is it true that $f(p)/p \\to 0$ for $p \\to \\infty$ in a density 1 subset of the primes? ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-parts-ii-93f31f53eb20078bf48ee25dd1aa6420-problem","reward_target_id":"fc-target:Erdos1072.erdos_1072.parts.ii","tasks":[{"task_id":"fc-v2-parts-ii-f763b86dbdaf5a4cf8c164f3-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:5d834fa4a05184e5c476e1cb7c1af362e2e5c93b65f82847bf060e5eb3888fd2","attempts":0},{"task_id":"fc-v2-parts-ii-070624a94b1dbe4b9a6ee731-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:1aab81adb30d2375f8f995c83d6478482da470a8cb086c15907abe62598e99b7","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-25T00:17:00Z","solved_at":null,"attempts":0},{"slug":"erdos1073-erdos-1073","display_title":"Erdős problem 1073","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1073","qualifier":null},"title":"Erdos1073.erdos_1073","statement":"True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ (x : ℕ), Erdos1073.A x ≤ ↑x ^ o x","summary":"Is it true that $A(x) \\le x^{o(1)}$? ","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[11],"is_open":true,"problem_id":"fc-33b3c405-erdos1073-erdos-1073-e9eba71a49efdafd1192302436462fd0-problem","reward_target_id":"fc-target:Erdos1073.erdos_1073","tasks":[{"task_id":"fc-v2-erdos1073-erdos-1073-3300f6de17be0ccd288598dc-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:92d0654f7d93168f12b0975da65185accfb9cb6d6252161309dfb29c34a4002b","attempts":0},{"task_id":"fc-v2-erdos1073-erdos-1073-91fad05b0e0125e4ae43fcec-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:92f766bd956ab720721b6cb900ab773df263ac68472f229883f89fae516f81c4","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-08-25T00:17:00Z","solved_at":null,"attempts":0},{"slug":"erdos108-erdos-108","display_title":"Erdős problem 108","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"108","qualifier":null},"title":"Erdos108.erdos_108","statement":"True ↔\n  ∀ r ≥ 4,\n    ∀ k ≥ 2,\n      ∃ f,\n        ∀ (V : Type u) (G : SimpleGraph V),\n          Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k","summary":"For every r ≥ 4 and k ≥ 2 is there some finite f(k,r) such that every graph of chromatic number ≥ f(k,r)\ncontains a subgraph of girth ≥ r and chromatic number ≥ k?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[5],"is_open":true,"problem_id":"fc-33b3c405-erdos108-erdos-108-acecd1eb94d4812b1571efc7dab188d7-problem","reward_target_id":"fc-target:Erdos108.erdos_108","tasks":[{"task_id":"fc-v2-erdos108-erdos-108-bdcb9352936e167f3ba5e8d1-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:9c059cc29865160f7411e4c7659a83911bbf533abd357760f02461604901c37c","attempts":0},{"task_id":"fc-v2-erdos108-erdos-108-ab8964d8ed5a4ea6b7682063-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:38837380d2d2545fc4f278e4320aee702fcc8c195a5e8091995b8db72185d3a9","attempts":0}],"bounty":{"amount_rao":null,"amount_usd":null,"policy_version":"linear-age-v3-chat-logs","available":false,"reason":"ALREADY_SOLVED","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"solved","accepting_submissions":false,"added_at":"2026-08-25T00:17:00Z","solved_at":"2026-09-16T20:29:30.171876Z","attempts":1},{"slug":"erdos1082-erdos-1082-parts-i","display_title":"Erdős problem 1082 - part i","title_parts":{"collection":"erdos_problems","collection_label":"Erdős problems","reference":"1082","qualifier":"part i"},"title":"Erdos1082.erdos_1082.parts.i","statement":"True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ distinctDistances A","summary":"Let $A\\subset \\mathbb{R}^2$ be a set of $n$ points with no three on a line.\nDoes $A$ determine at least $\\lfloor n/2\\rfloor$ distinct distances?\n","category":"research open","classification":"DIRECT_PROP","task_modes":["formalized","counterexample"],"tier":"tier-1","ams_subjects":[51],"is_open":true,"problem_id":"fc-33b3c405-parts-i-291b54e13cd0e9fc22499e99155e73cd-problem","reward_target_id":"fc-target:Erdos1082.erdos_1082.parts.i","tasks":[{"task_id":"fc-v2-parts-i-ed1e02071af3890e7b023b1e-formalized","task_mode":"formalized","task_bundle_sha256":"sha256:40df59a18286774295a659a8abb81d8a36d42e6e301e84e78070d2a86f2afeee","attempts":0},{"task_id":"fc-v2-parts-i-e657739602b38d234abe226e-counterexample","task_mode":"counterexample","task_bundle_sha256":"sha256:16a7b78f4246cf4d3d68d4d8ac0d64e590aaecf99658386a5a86995d91f2220d","attempts":0}],"bounty":{"amount_rao":8213457061999,"amount_usd":"3443.79","policy_version":"linear-age-v3-chat-logs","available":true,"reason":"OPEN","as_of":"2026-11-15T23:37:00Z","locked":false},"display_status":"open","accepting_submissions":true,"added_at":"2026-09-08T06:03:00Z","solved_at":null,"attempts":0}],"facets":[{"field":"category","values":[{"value":"research open","count":327}]},{"field":"classification","values":[{"value":"DIRECT_PROP","count":327}]},{"field":"task_mode","values":[{"value":"counterexample","count":327},{"value":"formalized","count":327}]},{"field":"tier","values":[{"value":"tier-1","count":327}]},{"field":"ams_subject","values":[{"value":"3","count":1},{"value":"5","count":71},{"value":"11","count":230},{"value":"12","count":2},{"value":"15","count":4},{"value":"20","count":1},{"value":"28","count":1},{"value":"30","count":1},{"value":"33","count":1},{"value":"37","count":1},{"value":"40","count":1},{"value":"51","count":2},{"value":"52","count":18},{"value":"60","count":1},{"value":"68","count":1},{"value":"94","count":1}]}],"repository_commit":"33b3c405cc7f6499595ce65c50e86be40354d372","limit":25,"offset":0}