Stream: condensed mathematics
Topic: reasonably easy sorries
Johan Commelin (Apr 15 2021 at 04:08):
thm95/constants.lean I've marked 3
sorrys as doable (around lines 150--160). This involves proving some inequalities between some real numbers.
breen_deligne/eg.lean there are 4
sorrys. This involves constructing 2 sequences of nonnegative reals, and proving that they satisfy certain inequalities.
I think both sets of sorries are doable by anyone who has a little bit of experience with Lean and real numbers. So if you are looking to make a small contribution to this project, feel free to try your hand at them.
Damiano Testa (Apr 15 2021 at 05:32):
Johan, I am taking look right now at these
Johan Commelin (Apr 23 2021 at 17:49):
The "doable" sorrys in
thm95/constants.lean have been done. Half of the Breen-Deligne constants has also been done.
Johan Commelin (Apr 28 2021 at 14:43):
For the record: the remaining sorrys are now also done.
Johan Commelin (Apr 28 2021 at 14:44):
In particular, there are now explicit sequences
c' for the explicit BD data.
Last updated: May 09 2021 at 15:11 UTC