Zulip Chat Archive

Stream: condensed mathematics

Topic: reasonably easy sorries

Johan Commelin (Apr 15 2021 at 04:08):

In thm95/constants.lean I've marked 3 sorrys as doable (around lines 150--160). This involves proving some inequalities between some real numbers.

In 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 sorrys!

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_ and c' for the explicit BD data.

Last updated: Dec 20 2023 at 11:08 UTC