triangle

Stream: new members

[vxctyxeha]

I tried to prove some IMO geometry problems, but it seems that mathlib doesn't have a definition of the incenter of a triangle. How do you define the incenter of a triangle?

[Weiyi Wang]

docs#Affine.Simplex.incenter
this one?

[Joseph Myers]

Note that I currently have 16 open PRs needing review in my series working towards IMO 2024 P4 (and there will be at least 6 more PRs in that series, including the final one with the actual solution to IMO 2024 P4 itself, before it's done).

In particular, you're unlikely to get far on many problems with the incenter without #30982, relating to angle bisection, which has been open since October and depends on #30981 (also open since October, all dependencies now merged). Other open PRs in this series specifically involving the incenter include #31057, #31733, #31981 (which has several unmerged dependencies).

At this point you should expect that formalizing a solution to an IMO geometry problem will involve opening at least tens of PRs along the way with more generally useful definitions or lemmas that were missing from mathlib, unless the requirements for that particular problem are extremely close to those of previously formalized problems.

You should also expect that most of the length of a formal solution will be proving nondegeneracy conditions, along with configuration properties such as the order of points on a line or which points are on the same side / opposite sides of a line or which angles are oriented the same way, rather than the parts corresponding more directly to the steps that are explicit in the informal solution.

[Weiyi Wang]

good old "it's obvious from the diagram"