# Zulip Chat Archive

## Stream: new members

### Topic: Hello! Have a proof of Heron's Area Formula!

#### Matt Kempster (Mar 31 2021 at 21:23):

Hi all! I discovered lean a couple days ago and have been thoroughly enjoying it. I noticed that Heron's Area Formula was on the list of missing theorems of the big 100, so as a fun experiment I attempted a proof. Lo and behold, I actually managed to do it!

Warning: The proof is incredibly, terribly messy. I know it can be simplified drastically - I will have fun doing that soon! But I was excited that I had killed my last `sorry`

and want to share:

https://github.com/matt-kempster/mathlib/commit/a9981fde5877c78edfa70e64bd99ce225dc1a4f2

Let me know if you have any pointed feedback - ways to rewrite sections, etc. I will be opening a PR soon; first I must:

- Extract the proof into the archive directory (instead of being inlined into geometry.lean
- Clean it up (obviously)
- Double-check that I actually proved the right thing/formulated it correctly/don't need to prove anything else

Thanks for reading!

P.S.: hello! Good to be here! :D

#### Bryan Gin-ge Chen (Mar 31 2021 at 21:25):

Welcome! Heron's area formula might well deserve to be in the main library rather than the archive, actually.

#### Heather Macbeth (Mar 31 2021 at 21:41):

Ideally, someday, the LHS of your equation will be `volume (convex_hull {p1, p2, p3})`

, where `volume`

is a measure naturally induced on the affine Euclidean space in question, coming from the Euclidean inner product.

#### Matt Kempster (Mar 31 2021 at 21:44):

Agreed, that's how the other theorem provers seem to be doing it. I wonder if Freek is okay with this formulation or not :)

#### Heather Macbeth (Mar 31 2021 at 21:44):

In my mind the main point would be that a real inner product (element of $\operatorname{Sym}^2V^*$) induces a volume form (element of $\Lambda^nV^*$). @Eric Wieser might be able to comment on how far away this is ...

#### Heather Macbeth (Mar 31 2021 at 21:45):

Is this also how other theorem provers do it? Or is it a more concrete construction of the associated measure? (I don't know if the other theorem provers have much in the way of tensors, etc.)

#### Eric Wieser (Mar 31 2021 at 21:47):

I think that @Amelia Livingston has more to say about exterior powers than I do

#### Matt Kempster (Mar 31 2021 at 21:47):

I just looked. It appears that HOL Light and Isabelle use the convex hull formulation, while Metamath, Coq, and Mizar all use the same formulation I did (based on distances between three points).

#### Eric Wieser (Mar 31 2021 at 21:48):

Although exterior powers over a dual space (if that's what the * is) are isomorphic to docs#alternating_map, right?

#### Heather Macbeth (Mar 31 2021 at 21:48):

Matt Kempster said:

I just looked. It appears that HOL Light and Isabelle use the convex hull formulation, while Metamath, Coq, and Mizar all use the same formulation I did (based on distances between three points).

What is the measure on the space in which the convex hull is taken? Effectively, is the space itself R^n (with the product measure) or a general affine Euclidean space?

#### Matt Kempster (Mar 31 2021 at 21:51):

Heather Macbeth said:

What is the measure on the space in which the convex hull is taken? Effectively, is the space itself R^n (with the product measure) or a general affine Euclidean space?

I'm no expert in either of those theorem provers, but it looks like they both use R^2:

#### Heather Macbeth (Mar 31 2021 at 21:51):

If you work in $\mathbb{R}^2$, we do have the measure, but you lose all the nice geometric expression. A little unsatisfactory either way :)

#### Heather Macbeth (Mar 31 2021 at 21:52):

(To be clear, it's our library that's unsatisfactory, not your proof!) :big_smile:

#### Kevin Buzzard (Mar 31 2021 at 21:53):

@Matt Kempster Freek told me that he explicitly avoids saying precisely how the theorem should be formalised and is happy if different people interpret a result in different ways. I think at least one of the proofs of Pythagoras's theorem just points to a definition of a norm on R^2 for example.

#### Heather Macbeth (Mar 31 2021 at 21:55):

Eric Wieser said:

Although exterior powers over a dual space (if that's what the * is) are isomorphic to docs#alternating_map, right?

@Eric Wieser Yes, so we want a construction of the alternating map induced by an inner product, and also a construction of the measure induced by an alternating map to the scalar field.

#### Heather Macbeth (Mar 31 2021 at 21:59):

Actually, sorry, it's more complicated. An inner product induces an element of $(\Lambda^nV^*)^{\otimes 2}$. This determines a density, and hence a measure, where a density is defined to be a $\pm$-equivalence class of elements of $\Lambda^nV^*$.

#### Eric Wieser (Mar 31 2021 at 22:02):

The closest I can offer right now for alternating maps derived from a quadratic form is the `clifford_algebra.ι_wedge`

definition in my repo

#### Eric Wieser (Mar 31 2021 at 22:04):

Square the result of that, and conjure an inverse algebra map, and I think you have your volume (squared)

#### Heather Macbeth (Mar 31 2021 at 22:05):

What do you mean by "square" here? It's clear if the object is an element of the top exterior power, and squaring produces an element of the tensor square of the top exterior power; it's less clear to me what is meant if the object is an alternating map.

#### Eric Wieser (Mar 31 2021 at 22:06):

I mean square the output after applying the map I guess

#### Eric Wieser (Mar 31 2021 at 22:07):

Which maybe doesn't make much sense if we're working with alternating maps only as a conveniently isomorphic object

#### Eric Wieser (Mar 31 2021 at 22:14):

Having actual exterior power objects in mathlib would certainly make this clearer!

#### Joseph Myers (Apr 01 2021 at 00:20):

The convention used for geometry results in mathlib is that you have `{V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]`

, so an arbitrary (possibly infinite-dimensional) Euclidean space, and then if the result is specific to two dimensions you have a two-dimensional subspace `{s : affine_subspace ℝ P} [finite_dimensional ℝ s.direction] (hd : findim ℝ s.direction = 2)`

and hypotheses that points are in it. Then you possibly have a variant of the result when the whole space is two-dimensional, for convenience of people using it in that context. (E.g. when stating an IMO geometry problem it makes sense to have `[finite_dimensional ℝ V] (hd2 : findim ℝ V = 2)`

rather than embedding the plane in a possibly larger space.) (When working with a triangle, you don't need those extra hypotheses, but you would if e.g. dealing with four points that must be coplanar.)

I think area in Heron (in mathlib proper) ought to be using the measure theory part of the library. To give and justify a definition of area/volume for an arbitrary Euclidean (affine) space by reference to one for `euclidean_space ℝ (fin n)`

(I'm not sure how close what we have on product measures is to giving us the latter), you need (a) an isometry from the arbitrary space to the `euclidean_space`

(which we have, more or less, given an isometry between `P`

and `V`

from `vadd_const`

etc. together with `linear_isometry_equiv.of_inner_product_space`

) and (b) a proof that the measure on the `euclidean_space`

is invariant under isometries, which I don't think we have, to show the definition is genuinely independent of the arbitrary choice of isometry used. (More generally, we ought to have that any affine map multiplies the measure by the absolute value of the determinant.)

Then you have the matter of expressing results on area / volume in a way that makes sense for a two-dimensional triangle in a larger-dimensional space, so want a notion of two-dimensional measure meaningful in that context (and to show it's equal to measure in a two-dimensional space when you use coercions to treat the subspace as a Euclidean space itself; I'm not sure we have all those coercions yet). (As an example of why that generality is useful, clearly we ought to have the result that the volume of a (possibly degenerate) n-dimensional simplex is equal to 1/n * volume of base * height, which is talking about both (n-1)-dimensional and n-dimensional volumes in the same space.)

I think convex hull makes sense as the thing you are taking the measure of (see Yury's past unfinished attempts to redo convexity in mathlib for affine spaces, #2910).

In the absence of being a statement about areas in a form properly linked to the measure theory part of the library, maybe the archive is a better place for the proof (with a view to being moved into mathlib proper once linked with measure theory).

#### Joseph Myers (Apr 01 2021 at 00:25):

Also, Heron (in a form going in mathlib proper) shouldn't have the hypotheses you have that the points are different; it's true for all degenerate triangles as well, and might sometimes be useful in degenerate cases.

#### Heather Macbeth (Apr 01 2021 at 00:33):

@Matt Kempster, by the way, I don't know if you have seen the proof for the area of a disc, by James Arthur, Ben Davidson and Andrew Souther:

https://github.com/leanprover-community/mathlib/blob/cc9915282edc5c432650e4838535cdef9f65c086/archive/100-theorems-list/9_area_of_a_circle.lean#L75

They take the opposite approach from you (with the opposite "problem"): it's stated using measure theory for a disc in `ℝ × ℝ`

(so someday it will also generalize to `metric.ball`

in a Euclidean affine space).

#### Matt Kempster (Apr 01 2021 at 00:33):

Joseph Myers said:

Also, Heron (in a form going in mathlib proper) shouldn't have the hypotheses you have that the points are different; it's true for all degenerate triangles as well, and might sometimes be useful in degenerate cases.

This is true, I was thinking about this. I suppose a workaround would be to define the area of a degenerate triangle as 0, right?

#### Joseph Myers (Apr 01 2021 at 00:34):

I think any reasonable definition should result in the area of a degenerate triangle being 0 without needing to special-case it in the definition (even if sometimes special cases are needed in the proofs).

#### Matt Kempster (Apr 01 2021 at 00:35):

Heather Macbeth said:

Matt Kempster, by the way, I don't know if you have seen the proof for the area of a disc, by James Arthur, Ben Davidson and Andrew Souther:

https://github.com/leanprover-community/mathlib/blob/cc9915282edc5c432650e4838535cdef9f65c086/archive/100-theorems-list/9_area_of_a_circle.lean#L75

They take the opposite approach from you (with the opposite "problem"): it's stated using measure theory for a disc in`ℝ × ℝ`

(so someday it will also generalize to`metric.ball`

in a Euclidean affine space).

Neat! By opposite "problem" you mean that it uses measure theory and wants to one day be part of Euclidean world, whereas my Heron proof is in Euclidean world and will one day be part of measure theory land?

#### Heather Macbeth (Apr 01 2021 at 00:35):

Precisely!

#### Matt Kempster (Apr 01 2021 at 03:39):

I have opened #6988 for this, after a lot of simplification and refactoring. I'm actually rather happy with the proof now!

My questions (copy-pasted from the PR, comment there if you'd like):

- Is there a linter I can run?
- Do you have any feedback on the proof style? Let me know where I can simplify or improve things.
- What is the deal with the required rotate, { exact V }, { exact _inst_1 }, that I have, and what do those lines do? Can I get rid of those extra 2 goals?

Also, hi to the following people whose names I recognize in here:

- @Jalex Stark
- @Aaron Anderson
- @Henry Swanson
- @Bolton Bailey

What a cool coincidence that you guys are here!!

#### Matt Kempster (Apr 01 2021 at 03:51):

Oh, I've just realized that I didn't do the workflow properly; I worked on a branch of a fork, instead of a branch of the main repository. Is this OK, or should I kill my PR and make a new one?

My github username is `matt-kempster`

- could I have access to create new branches of mathlib? Thanks!

#### Bryan Gin-ge Chen (Apr 01 2021 at 03:55):

Yes, please open a PR from the main repository. I've just sent you an invitation: https://github.com/leanprover-community/mathlib/invitations

#### Bryan Gin-ge Chen (Apr 01 2021 at 03:57):

We have two linters that are run by our CI scripts. To run them locally, see this post.

#### Matt Kempster (Apr 01 2021 at 03:59):

Thanks for the tips, Bryan.

Opened #6989. Feel free to review!

Last updated: May 14 2021 at 00:42 UTC