# 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 `sorry`

s as doable (around lines 150--160). This involves proving some inequalities between some real numbers.

In `breen_deligne/eg.lean`

there are 4 `sorry`

s. 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 `sorry`

s!

#### 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: May 09 2021 at 15:11 UTC