The Area of a Circle (metamath 100 #9)

[metamath]

The Area of a Circle (metamath 100 #9)

[Achaemenid]

Done. It's messy - not yet minimized, plus I'll probably rewrite lemma 4 to be based on resqrcn (which I hadn't realized existed) - and relies on countable choice (couldn't really do it without FTC, whose formulation relies on countable choice), but it's valid.

[tirix]

Congratulations!
And proof shortening seems to be on its way, too!

[david-a-wheeler]

Wow, and fantastic. I'm waiting to hear from Norm or Mario, but if they day "ok" I'm looking forward to adding this to the list of proofs completed.

[nmegill]

Hi Achaemenid, This is a great job! There are some minor administrative and cosmetic issues to be addressed: 1. The pull request should be for updating develop, not master. 2. Currently we don't keep mathboxes as separate files. (That is a long discussion, and someday we will have to when set.mm grows too large, but not yet.) So you should place your mathbox into set.mm as the second one, between David Abernathy's and Stefan Allen's, and it is that modified set.mm for which you will create a pull request. 3. Even though Travis says "no errors", that is because it checks only set.mm and not other files. You can check for most errors locally by running "verify markup */f", which it does not pass now (lines too long, contributor field "?who?" not updated). 4. It may need to be updated to be compatible with the latest set.mm on develop, which has had a number of changes since the last master release (mostly label changes). You can see the label changes in the list at the top of set.mm. 5. Is "Achaemenid" is a pseudonym? Traditionally we have encouraged people to use real names for the contributor, but if you prefer a pseudonym we will use it. (There have been two other pseudonymous contributors that I'm aware of, including the venerable Mel L. O'Cat.) I will add Achaemenid as a contributor at the top of set.mm with initials AM, if that is what you prefer. I hope these can be resolved soon, because I'm eager to update set.mm and put it on the web site! Thanks, Norm

…

On 9/1/17 2:34 PM, David A. Wheeler wrote: Wow, and fantastic. I'm waiting to hear from Norm or Mario, but if they day "ok" I'm looking forward to adding this to the list of proofs completed. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#89 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AMKLqNTO9mskjhTDJnaFy5vQJ18U0vfAks5seE4dgaJpZM4LJwRv>.

[Achaemenid]

I was going to take you up on your offer, yearning as I do for the Internet of yore, but I've posted enough on the Google Group that I'm pretty sure some people have figured out who I am already, and certainly would if I kept at this. There was a time... but that time is long gone. Put me down as "Brendan Leahy."

For some reason, dvreasin and areacirclem6 didn't auto-generate "Contributed by..." statements, and even though I tried to write them in, "verify markup" won't accept them. Dunno what's wrong.

[david-a-wheeler]

Fantastic! This is done, so closing.