Skip to content

feat(OEIS/80170): mark conjecture as solved #4253

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
mo271 merged 3 commits into from
Jun 24, 2026
+13 −3
Merged

feat(OEIS/80170): mark conjecture as solved #4253

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4e4ebbb
feat(OEIS/80170): mark conjecture as solved
guodk Jun 12, 2026
33af73c
docs(OEIS/80170): cite Stephan and the proof preprint, attribute proo…
guodk Jun 23, 2026
8abd9e5
Merge branch 'main' into mark-80170-solved
mo271 Jun 24, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 11 additions & 1 deletion FormalConjectures/OEIS/80170.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,18 @@ def PrimePowerCondition (k : ℕ) : Prop :=

/--
Conjecture: The gcd condition is equivalent to the prime power condition.

@mo271 mo271 Jun 13, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
Conjecture: The gcd condition is equivalent to the prime power condition.
Conjecture: The gcd condition is equivalent to the prime power condition.
This has been conjectured by Ralf Stephan.

This is prexisting and should hvae been added when this conjecture was added: but let's mention that this conjecture was added to the OEIS by Ralf Stephan, (who is also a frequent contributor to our repo under the github hanble @rwst !)

This has been conjectured by Ralf Stephan.

Both the natural-language proof and its Lean 4 formalization were carried out
by the KLMM MechMath Agent Team; see the `formal_proof` attribute.

*References:*
- [Ralf Stephan, *Prove or Disprove. 100 Conjectures from the OEIS*, 2004, Conjecture 17 (arXiv:math/0409509)](https://arxiv.org/abs/math/0409509)
- [Dakai Guo et al., *A Greatest Common Divisor Criterion of Certain Binomial Coefficients*, 2026 (arXiv:2606.22997)](https://arxiv.org/abs/2606.22997)
-/
@[category research open, AMS 11]
@[category research solved, AMS 11,
formal_proof using formal_conjectures at
"https://github.com/guodk/formal-conjectures/blob/0720658844d76a50d48e4baa152eef14d4462907/FormalConjectures/OEIS/80170.lean#L1823"]
theorem gcdCondition_iff_primePowerCondition (k : ℕ) (hk : 2 ≤ k) :
GCDCondition k ↔ PrimePowerCondition (k + 1) := by
sorry
Expand Down
4 changes: 2 additions & 2 deletions FormalConjectures/Subsets/FC100OpenSet1.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,6 +221,6 @@ end Subsets.FC100OpenSet1

open Lean Meta ProblemAttributes in
#eval verifyCategoryCounts Subsets.FC100OpenSet1.problems [
("research open", 96),
("research solved", 4)
("research open", 95),
("research solved", 5)
]
Loading