Skip to content

feat(Wikipedia): add Scholz conjecture#4365

Open
eyang07 wants to merge 6 commits into
google-deepmind:mainfrom
eyang07:issue-2217-scholz-conjecture-pr
Open

feat(Wikipedia): add Scholz conjecture#4365
eyang07 wants to merge 6 commits into
google-deepmind:mainfrom
eyang07:issue-2217-scholz-conjecture-pr

Conversation

@eyang07

@eyang07 eyang07 commented Jul 1, 2026

Copy link
Copy Markdown
Contributor

Closes #2217.

Tested with: lake --wfail build FormalConjectures.Wikipedia.ScholzConjecture.

@github-actions

github-actions Bot commented Jul 1, 2026

Copy link
Copy Markdown

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

  • Please take a look at the style guidelines,
    especially the conventions for references, categories, AMS tags, and answer(sorry).
  • You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
  • This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

@google-cla

google-cla Bot commented Jul 1, 2026

Copy link
Copy Markdown

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

@eyang07 eyang07 force-pushed the issue-2217-scholz-conjecture-pr branch from 0307702 to 87ccd4f Compare July 1, 2026 04:27

@jeangud jeangud left a comment

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.

Thank you @eyang07 for the contribution! This looks good as a first pass.

A few initial minor comments and maybe an alternative for IsAdditionChain.

Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
Comment thread FormalConjectures/Wikipedia/ScholzConjecture.lean Outdated
eyang07 and others added 5 commits July 4, 2026 11:55
Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com>
Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com>
Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com>
Co-authored-by: Jean-Guillaume Durand <113947520+jeangud@users.noreply.github.com>
- Use LaTeX syntax for math in docstrings
- Drop the getElem? implementation note from IsAdditionChain's docstring
- Remove the duplicated problem statement from the top-level docstring;
  reuse the addition-chain description on IsAdditionChain
- Add the Tall (2022) reference (arXiv:2210.13812 / ePrint 2023/020)
@eyang07

eyang07 commented Jul 4, 2026

Copy link
Copy Markdown
Contributor Author

Thanks for the suggestions and review

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Scholz conjecture on addition chains

2 participants