The issue author says the lemmas are needed for Fermat's right-triangle theorem, and there is no PR. The proof risk is nearly zero; the remaining uncertainty is maintainer judgment about names, generality, and placement.
lemmaOn hold after campaign review
Add gcd lemmas for a coprime sum and difference
Add Mathlib lemmas showing the gcd of m+n and m−n is 1 for coprime integers of opposite parity and 2 for coprime integers of the same parity, with theorem placement and names agreed from issue #37366.
Both short Lean proofs are already posted in the issue and compile in Lean Live; the contribution must integrate them cleanly, pass Mathlib CI, and contain no new axioms or `sorry`.
- Difficulty
- 1/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4integer gcdcoprimalityparity
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.