Ceva theorem, first try

Stream: new members

[Anders Larsson]

I have tried to adapt the Ceva theorem proof from Metamath.

Available at: https://gist.github.com/anders-was-here/d786450daba4c01e40bbc5f81c681feb

Original proof/formalization by Saveliy Skresanov: http://us.metamath.org/mpeuni/cevath.html

[Arthur Paulino]

I really like the font you used in some comments btw. I think this is the first time I see it

[Anders Larsson]

Arthur Paulino said:

I really like the font you used in some comments btw. I think this is the first time I see it

It must be unicode. (I think Gists are pure text files). It's cut'n'paste from the Metamath page.

[Yaël Dillies]

Congrats! Have a look at #10632 and a chat with @Mantas Baksys

[Jun Akita]

Hi Lean Community!

My name is Jun Akita, majoring in fundamental mathematical theory and natural language processing.
I am not so familiar with Lean now, but I want to contribute completing mathlib library.
I will try to formalize Theorem Ceva for my graduation research.

My goal is to make an AI mathematician.
Developing Lean will help with achievement of this goal.

I'd love to hear your advice, what I should do or how difficult it is.

If you have similar research interests, I would be delighted to hear from you. I would very much look forward to the possibility of collaborating!

[Notification Bot]

A message was moved here from #new members > Algebraic Topology by Jun Akita.

[Joseph Myers]

If you want to prove Ceva in a form suitable for mathlib, see various past discussions on the topic; the main form would be for a n-simplex in an affine space that might be more than n-dimensional, and both Ceva and its converse would best be split up into little lemmas each with the weakest assumptions that work for those lemmas.