Added Odd Weird Number Conjecture#3498
Conversation
|
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. |
|
I have now signed the CLA. |
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Thanks for the contribution!
A first remark about re-using stuff from Mathlib
Co-authored-by: Aditya Ramabadran <adihaya@gmail.com>
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
LGTM, thanks!
We already have that as Erdős problem 470, but it is still good to have here.
Potentially also good to add the wikipedia reference and oeis to the file in ErdosProblems!
| @[category research open, AMS 11] | ||
| theorem existence_odd_weird : | ||
| answer(sorry) ↔ ∃ n : ℕ, n.Weird ∧ Odd n := by | ||
| sorry |
There was a problem hiding this comment.
| sorry | |
| theorem existence_odd_weird : type_of% Erdos.470.erdos_470.part1 := by | |
| sorry |
| import FormalConjectures.Util.ProblemImports | ||
|
|
There was a problem hiding this comment.
| import FormalConjectures.Util.ProblemImports | |
| import FormalConjectures.Util.ProblemImports | |
| import FormalConjectures.ErdosProblems.«470» |
This is already here, but still good to also have the wikipedia file!
mo271
added
the
awaiting-author
3 participants
Fixes #2250