# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Statement of Cauchy's integral formula

#### Kevin Buzzard (Jun 28 2020 at 00:28):

Do we have the statement of Cauchy's Integral Formula in Lean? If not, would this be relatively easy to knock up, possibly with some stub definition of what continuity class the curve needed to be in?

#### Kevin Buzzard (Jun 28 2020 at 00:33):

If we could turn this into a theorem with a `sorry`

proof, even if we use undefined constants, it would be a really cool summer project for the hoardes at the discord. I don't trust myself to formalise the statement, because I don't understand the implementation decisions that have been made. I don't want to be making levels, I want to be proving theorems. If the experts could formalise the statement it would be brilliant. If you use an undefined typeclass like [is_smooth_curve] or whatever, then we could just skip the proof that the closed unit disc is a closed curve, for example. If there is more than one possibility for setting this question up, and you think it's worth an experiment, then just guess one and we can try it.

#### Yury G. Kudryashov (Jun 28 2020 at 03:55):

Please ping me about it tomorrow. I have some old code with outline of the proof of a version of this theorem but it needs much better `integral`

s library.

#### Kevin Buzzard (Jun 28 2020 at 04:22):

I want to go top down so this would be perfect

Last updated: May 17 2021 at 15:13 UTC