This might be relevant to some other mailing lists as well.
> Anfang der weitergeleiteten Nachricht: > > Von: Ken Kubota <m...@kenkubota.de> > Betreff: Aw: [isabelle] New in the AFP: Eudoxus Reals > Datum: 4. November 2023 um 03:34:06 MEZ > An: "Prof. Lawrence C. Paulson" <l...@cam.ac.uk> > Kopie: isabelle-users <cl-isabelle-us...@lists.cam.ac.uk> > > I have to say that I find it inappropriate to continue with routine work > currently. > > The New York U.N. representative wrote concerning Gaza: "This is a text-book > case of genocide.“ > > https://www.documentcloud.org/documents/24103463-craig-mokhiber-resignation-letter > > This is confirmed by brilliant analysts such as the former CIA analyst Ray > McGovern: > > https://odysee.com/@SputnikInternational:c/New-Rules-Ray-McGovern:f?t=100 > > Doesn’t the University of Cambridge officially condemn this act of genocide? > > While generally science should be autonomous to a certain degree, there are > limits. > Particularly in times where public protests effectively can make a difference. > > Bertrand Russell wasn’t indifferent: > https://sonar21.com/lord-bertrand-russells-on-israels-miscalculation/ > > Some more information is provided below. > > ____________________________________________________ > > Ken Kubota > https://doi.org/10.4444/100 > > > > Links: > > https://marlene.hilsenrath.de/blog/gaza-genocide/ > > https://www.mintpressnews.com/craig-murray-israel-genocide-gaza-regional-war-unavoidable/286129/ > https://odysee.com/@SputnikInternational:c/New-Rules-Ray-McGovern:f?t=100 > https://www.ohchr.org/en/press-releases/2023/10/gaza-un-experts-decry-bombing-hospitals-and-schools-crimes-against-humanity > https://rumble.com/v3r6kw7-judge-napolitano-judging-freedom-ray-mcgovern-blinken-goes-berserk.html?start=468 > https://rumble.com/v3poopd-judge-napolitano-judging-freedom-us-aid-is-destroying-ukraine.-w-ray-mcgove.html?start=588 > https://odysee.com/@LandDestroyer:8/the-2009-us-plan-for-iran-war-sees-new:d > https://www.youtube.com/live/iq1SjC7u8l0?t=126 > https://www.sevimdagdelen.de/toedliche-doppelmoral/ > https://www.documentcloud.org/documents/24103463-craig-mokhiber-resignation-letter > > > From: https://www.tiktok.com/@marlenehilsenrath/video/7297390486308818208 > > > >> Am 01.11.2023 um 17:45 schrieb Lawrence Paulson <l...@cam.ac.uk>: >> >> I am happy to announce a new AFP entry, by Ata Keskin: >> >>> Eudoxus Reals >> >>> Similar to the classical method of Dedekind cuts, our approach starts from >>> first principles. However, unlike Dedekind cuts, Eudoxus reals directly >>> derive real numbers from integers, bypassing the intermediate step of >>> constructing rational numbers. This construction of the real numbers was >>> first discovered by Stephen Schanuel. Schanuel named his construction after >>> the ancient Greek philosopher Eudoxus, who developed a theory of magnitude >>> and proportion to explain the relations between the discrete and the >>> continuous. Our formalization is based on R.D. Arthan's paper detailing the >>> construction. For establishing the existence of multiplicative inverses for >>> positive slopes, we used the idea of finding a suitable representative from >>> Sławomir Kołodyńaski's construction on IsarMathLib which is based on >>> Zermelo-Fraenkel set theory. Up to this date, our formalization is the only >>> construction of Eudoxus reals which is based on HOL. >> >> Curiously enough, I've wanted to see this sort of construction for several >> decades. NG de Bruijn once mentioned to me his own construction of the real >> numbers without the rationals: >> >> N.G de Bruijn, >> Defining reals without the use of rationals, >> Indagationes Mathematicae Volume 79, Issue 2, 1976, >> https://doi.org/10.1016/1385-7258(76)90055-X. >> >> Interesting references in that paper, too. So thanks to Ata! >> >> Anyway, the entry is online at >> https://www.isa-afp.org/entries/Eudoxus_Reals.html >> >> Larry Paulson >> >> >> >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
