robinzfc
Theorem. $\sqrt{2}$ is irrational.
Proof.
Assume that $\sqrt{2}$ is rational. Then there are integers $a, b$ such that $a^2=2b^2$ and $(a,b)=1$. Hence $a^2$ is even. Therefore $a$ is even. So there is an integer $c$ such that $a=2c$. Then $4c^2=2b^2$ and $2c^2=b^2$. So $b$ is even. Contradiction.
Qed.
Or, say Isar in Isabelle/ZF [2].
There is an interesting discussion on MathOverflow titled "Are we stuck with Lean?" [3]. The conclusion seems to be yes, they are.
[1] https://ceur-ws.org/Vol-448/paper10.pdf
[2] https://isarmathlib.org/UniformSpace_ZF_1.html
[3] https://mathoverflow.net/questions/513742/are-we-stuck-with-...
[1] https://github.com/MizarProject/system [2] https://github.com/digama0/mizar-rs [3] https://arxiv.org/pdf/2304.08391v2 [4] https://link.springer.com/article/10.1007/s10817-018-9479-z
The example papers [1] [2] [3] [4] have 18 unique co-authors. Also, it's Beatriz.
> she makes analysis of several pairs of pictures
"We base our analysis on the catalog of 298,165 short-duration transients presented in Solano et al. (2022), detected in 200 red POSS-I plates with typical exposure times of 45–50 minutes." [1]
"Of the 2,718 days in this period, transients were observed on 310 days (11.4%)" [2]
"These searches significantly reduced the number of candidates (from 298 165 to 9 395)" [3]
> uniformly spread out across the whole plate
> thousands of uniformly spread out image defects
"we find a strong deficit of transient detections, at the 22 sigma statistical significance level, within the Earth’s umbral shadow" [1]
"we expect N = 1223 transients in shadow out of 106,339 total, corresponding to an expected fraction of fexp = 0.0115±0.00033. However, we observe only N = 349 transients in shadow" [1]
"Plate defects, by contrast, are expected to be randomly shaped and distributed" [1]
> in all pairs of plates the lights change one way only. On the first plate they are present and on the next plate 50 minutes later they disappear
"transients that appear only in one long exposure and are entirely absent shortly before and after" [1]
"In brief, transients were defined as distinct star-like point sources present in POSS-I E Red images that were absent both in images taken immediately prior to the POSS-I Red image and in all subsequent images." [2]
(*) POSS -- Palomar Observatory Sky Survey
[1] Aligned, multiple-transient events in the First Palomar Sky Survey, 2025, preprint
[2] Transients in the Palomar Observatory Sky Survey (POSS-I) may be associated with nuclear testing and reports of unidentified anomalous phenomena, Scientific Reports, 2025
[3] Discovering vanishing objects in POSS I red images using the Virtual Observatory, 2022, Monthly Notices of the Royal Astronomical Society, 515, 1380
[4] A glint in the eye: photographic plate archive searches for non-terrestrial artefacts, 2022, Acta Astronautica, 194, 106
Turns out looking for quotes directly contradicting debunker's statements is a great way to focus while reading a UAP-related scientific paper, thank you.
[1] https://mathoverflow.net/questions/291158/proofs-shown-to-be...
Some proof assistants contribute more directly to understanding by making proofs easier to study.
Metamath: https://us.metamath.org/mpeuni/mmset.html#axioms
Isabelle/ZF: https://isabelle.in.tum.de/dist/library/FOL/ZF/ZF_Base.html
[1] https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijecti...
[2] https://isarmathlib.org/func1.html#a_bij_def_alt
[3] https://mizar.uwb.edu.pl/forum/archive/2403/msg00001.html
"mitochondrial divergence values between H. diadema samples from the Solomon Islands and New Guinea were greater than any observed divergence values between H. diadema and H. dinops samples from within the Solomon Islands"
The paper describes an example of parallel evolution. There is one species of smaller bats (H.dinops) and then on different islands larger ones evolved from it independently. The bigger bats have all been called H. diadema as they look very similar. So the situation is more like "same size, different species" than what the title suggests.
[1] [Parallel evolution in an island archipelago ...](https://academic.oup.com/evolut/advance-article/doi/10.1093/...)
The Roman Empire lasted about 500 years - from 31 BC to the fall of the Western Roman Empire in 476. If we include the period of existence of the Eastern Roman Empire it would be almost 1500 years - until the fall of Constantinople in 1453.
Yes, there is, in 2022 it was in PIT 38, sec. E. You need to report purchases even when you have not sold anything as this entitles you to subtract cost when you sell later.