Ceva's theorem

Stream: mathlib4

[Felix Pernegger]

Hello, I hope this is not the wrong channel to write this (this is my first time here):
As part of a project, which itself is due to a course taught by @Floris van Doorn , I recently formalised Ceva’s theorem (number 61).
However I did not really use mathlib at all and redefined planar geometry (via complex numbers as foundation) by myself from scratch. Also warning, code quality is close to nonexistent…
On the other hand, the formalisation contains no sorry’s or anything like that.
I also formalised the converse and a special case (cevians being all parallel), resulting in, from what I can see, the most general form of the theorem in the planar / triangle case. For the main case I used the classical argument with areas.

The final statement appears to be more a bit general than the formalisations (by other proof assistants) listed for Ceva’s theorem in the 100 theorems list.

For the final statement see the very bottom of (theorem ceva):

https://github.com/felixpernegger/LeanCourse24/blob/master/LeanCourse/Project/Ceva.lean

[Ruben Van de Velde]

Nice! You should add a link to your repository to the 100.yaml file in mathlib! (If you haven't got push access to mathlib and weren't otherwise planning on contributing, someone else could do this too)

[Violeta Hernández]

FYI, Ceva's theorem should be a theorem in any vector space. That is, given three affinely independent points a, b, c, and three other points d, e, f which are convex combinations with coefficients r, s, t of the appropriate points, then ad, be, and cf intersect at a point iff r * s * t = 1.

[Yaël Dillies]

See below

Yaël Dillies said:

Michael Rothgang said:

I saw a PR about 61 (Ceva) a while back (6-12 months?), which was never merged. I can't find the PR on mathlib or mathlib4, though. Joseph Myers

It was Mantas Baksys and I. It's certainly close to completion. I could give it another stab

Joseph Myers said:

I don't think Ceva is close to completion, that PR is all specific to the case of triangles in a two-dimensional space (using affine bases), when nothing should require the simplex to be top-dimensional and most things shouldn't be specific to triangles either (triangles should just be a special case deduced at the end).

[Yaël Dillies]

The PR is !3#10632

[Kevin Buzzard]

For Freek 100 I think that any formalization of anything which seems like it could be interpreted as Ceva's theorem, even if it's not in mathlib, should be fine, so I would second Ruben's suggestion that you just add a link to your repo to 100.yaml .

[Michael Rothgang]

If you do so, can you also add it to 1000.yaml, please? Thanks a lot!

[Yaël Dillies]

If you're interested, here's a start at the formalisation of higher dimensional Ceva: https://github.com/YaelDillies/LeanCamCombi/tree/ceva EDIT: Now here: https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/Convexity/Ceva.lean

[Yaël Dillies]

Feel free to take it up from here

[Ruben Van de Velde]

I think someone should file an issue with the current thinking on what a mathlib-compatible formalisation of Ceva should look like

[Violeta Hernández]

Yaël Dillies said:

If you're interested, here's a start at the formalisation of higher dimensional Ceva: https://github.com/YaelDillies/LeanCamCombi/tree/ceva

What does higher dimensional Ceva say? I can't imagine how any part of the statement generalizes.

[Yaël Dillies]

Did you read my Lean statement? Alternatively, check the Wikipedia page on Ceva's theorem. I am doing the first generalisation they mention

[Violeta Hernández]

Sorry, got a bit lost in your repository...

That's a really cool version of the theorem, and it should also imply the triangle version, at least if you allow for negative masses and the like.

[Joseph Myers]

I'd expect a statement in mathlib to be for affine spaces not just vector spaces, there should be no real dependency on convexity. (Even for versions involving a point being in the interior of a simplex, I think it's reasonable to add a definition of the interior of a simplex not depending on convexity. The concept of the interior of a simplex is common enough to justify having a separate definition rather than always needing to say "interior of the convex hull", the definition could always be linked to convexity later after the convexity refactor is done, or linked now only in the vector space case but with the definition being available more generally.)

I concluded that the convexity refactor is not actually a dependency of any definitions needed for cleanly stating any past IMO geometry (or combinatorial geometry) problem - even when a problem talks about a convex polygon, definitions relating to convex sets don't really help for defining the property of a sequence of vertices being those of a convex polygon.

[Yaël Dillies]

Yaël Dillies said:

Did you read my Lean statement? Alternatively, check the Wikipedia page on Ceva's theorem. I am doing the first generalisation they mention

Now here: https://github.com/YaelDillies/MiscYD/blob/master/MiscYD/Convexity/Ceva.lean