[isabelle] Help with Triangulation

[Michal Wallace]

I am working on formalizing Euler’s relation between the number of
n-dimensional faces of a polytope (aka the polyhedron formula), and then
hopefully using this to derive Pick’s theorem for the area of polygons
whose vertices fall on integer lattice points in the plane.

I intend to approach both proofs using arguments based on induction over a
triangulation.

There are a couple theorems relating to triangulations in
HOL/Analysis/Polytope.thy but I suspect I will need to generalize and
refactor them a bit if they are to be useful for me.

For the first proof, in each step, I start with a convex polytope and want
to make a single cut that separates one of its vertices, leaving me with
two convex polytopes.

For the second proof, I want to start with an arbitrary simple polygon (not
necessarily convex), and end up with a bijection between lattice points in
the polygon and vertices in the triangulation. Here, instead of one cut
going all the way through the polygon at each step, I need to make several
small cuts as I add each new vertex to the triangulation.

Basically, I seem to need some fine grained control over how the
triangulation is performed.

Here is what I’m currently thinking:


1.

A “cell_complex” is a recursive data type, where each interior node
represents a (generic) cut, and each leaf represents a polytope.
2.

A “triangulation” is a subtype of “cell_complex” where each leaf is a
simplex.
3.

A “cut” is a type parameter to those type, so cuts can be hyperplanes in
one case, and lists of line segments in the other, and so other people can
apply the idea to their own ends.
4.

A ‘ cut strategy is a function of type:: polytope => ‘cut triangulation
=> ‘cut
5.

Finally, I provide some generic function (polytope => ‘cut strategy =>
‘cut triangulation) takes care of the actual construction.


My hope is that with this strategy, I will be able to:


1.

Reason inductively about relationships either the polytope or the
resulting triangulation:
1.

Proof 1 : Euler’s relation holds for polytopes in dimension D if it
holds in all dimensions < D and it holds for the two parts after making a
cut [1]
2.

Proof 2: certain relationships between the numbers of edges, interior
points, and boundary points hold for the triangulation itself,
as each new
point is added. [2]
2.

I will be able to execute the algorithms on actual polytopes that I
construct in code, and produce nice little diagrams for the final paper.


I’m a programmer by trade, so I’m pretty confident in my ability to handle
part 2. I’m not so certain about part 1.

So… I think I’m basically asking for a sanity check on this approach. Does
it make sense? Are there things I should be looking at that already do
something like this? Am I going to run into trouble mixing ideas from
programming and geometry like this? Should I try to refactor the theorems
in Polytope.thy or just start from scratch?

Or is there a better way of approaching this altogether?

Thanks!

For reference, the informal proofs I’m working from are:

Helge Tverberg, “How to cut a convex polytope into simplices”

https://vdocuments.site/documents/how-to-cut-a-convex-polytope-into-simplices.html

W.W. Funkenbusch, “From Euler’s Formula to Pick’s Theorem, using an Edge
Theorem”

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.475.919&rep=rep1&type=pdf

[Lawrence Paulson]

Thanks for your email. My name is at the top of Polytope.thy, but I'm afraid I don't know much about polytopes. I just ported this material from HOL Light. Pick’s theorem is also available in HOL Light, and from my perspective, the easiest way to reach it is by porting John Harrison's proof. That's because I'm very familiar with HOL Light's tactics, so this may not work for you. Nevertheless, there must be many valuable clues in the file pick.ml <https://github.com/jrh13/hol-light/blob/master/100/pick.ml>, and its prerequisites have already been reported.

Larry

Post by Michal Wallace
I am working on formalizing Euler’s relation between the number of
n-dimensional faces of a polytope (aka the polyhedron formula), and then
hopefully using this to derive Pick’s theorem for the area of polygons
whose vertices fall on integer lattice points in the plane.
I intend to approach both proofs using arguments based on induction over a
triangulation.
There are a couple theorems relating to triangulations in
HOL/Analysis/Polytope.thy but I suspect I will need to generalize and
refactor them a bit if they are to be useful for me.
For the first proof, in each step, I start with a convex polytope and want
to make a single cut that separates one of its vertices, leaving me with
two convex polytopes.
For the second proof, I want to start with an arbitrary simple polygon (not
necessarily convex), and end up with a bijection between lattice points in
the polygon and vertices in the triangulation. Here, instead of one cut
going all the way through the polygon at each step, I need to make several
small cuts as I add each new vertex to the triangulation.
Basically, I seem to need some fine grained control over how the
triangulation is performed.
1.
A “cell_complex” is a recursive data type, where each interior node
represents a (generic) cut, and each leaf represents a polytope.
2.
A “triangulation” is a subtype of “cell_complex” where each leaf is a
simplex.
3.
A “cut” is a type parameter to those type, so cuts can be hyperplanes in
one case, and lists of line segments in the other, and so other people can
apply the idea to their own ends.
4.
A ‘ cut strategy is a function of type:: polytope => ‘cut triangulation
=> ‘cut
5.
Finally, I provide some generic function (polytope => ‘cut strategy =>
‘cut triangulation) takes care of the actual construction.
1.
Reason inductively about relationships either the polytope or the
1.
Proof 1 : Euler’s relation holds for polytopes in dimension D if it
holds in all dimensions < D and it holds for the two parts after making a
cut [1]
2.
Proof 2: certain relationships between the numbers of edges, interior
points, and boundary points hold for the triangulation itself,
as each new
point is added. [2]
2.
I will be able to execute the algorithms on actual polytopes that I
construct in code, and produce nice little diagrams for the final paper.
I’m a programmer by trade, so I’m pretty confident in my ability to handle
part 2. I’m not so certain about part 1.
So… I think I’m basically asking for a sanity check on this approach. Does
it make sense? Are there things I should be looking at that already do
something like this? Am I going to run into trouble mixing ideas from
programming and geometry like this? Should I try to refactor the theorems
in Polytope.thy or just start from scratch?
Or is there a better way of approaching this altogether?
Thanks!
Helge Tverberg, “How to cut a convex polytope into simplices”
https://vdocuments.site/documents/how-to-cut-a-convex-polytope-into-simplices.html
W.W. Funkenbusch, “From Euler’s Formula to Pick’s Theorem, using an Edge
Theorem”
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.475.919&rep=rep1&type=pdf

[José Manuel Rodriguez Caballero]

Both Euler's formula its application to Pick's theorem are explained in a
very pedagogical way in chapter 12 of the following book:

Aigner, Martin, et al. *Proofs from the Book*. Vol. 274. Berlin: Springer,
2010. (You may find a link after a quickly search in google)

Concerning your question

Proof 1 : Euler’s relation holds for polytopes in dimension D if it

Post by Michal Wallace
holds in all dimensions < D and it holds for the two parts after
making a
cut [1] So… I think I’m basically asking for a sanity check on this
approach. Does
it make sense? Are there things I should be looking at that already do
something like this? Am I going to run into trouble mixing ideas from
programming and geometry like this?

This is the hard way to prove it. The easy way is to interprete Euler's
formula as a theorem in Graph Theory and then to deduce its application to
a polytope as a trivial corollary (see the book that I cited to find the
details). Dimension plays no essential role, because it is just a theorem
about a graph.

Concerning you observation:

I’m a programmer by trade, so I’m pretty confident in my ability to handle

Post by Michal Wallace
part 2. I’m not so certain about part 1.

In my case, I'm a mathematician by trade (Master degree), and the
programming part is what I am learning right now thanks to the people of
this mailing list. By the way, I'm open to consider any PhD position where
I can apply my mathematical skills to Isabelle or another proof assistant.

Kind Regards,
Jose M.




Message: 1

Post by Michal Wallace
Date: Sat, 11 Aug 2018 18:13:15 -0400
Subject: [isabelle] Help with Triangulation
<CAE6HCjn7tjCY6W48v_JdzgndOGEdhcUdrCons6wGZ3U1yJgU
Content-Type: text/plain; charset="UTF-8"
I am working on formalizing Euler’s relation between the number of
n-dimensional faces of a polytope (aka the polyhedron formula), and then
hopefully using this to derive Pick’s theorem for the area of polygons
whose vertices fall on integer lattice points in the plane.
I intend to approach both proofs using arguments based on induction over a
triangulation.
There are a couple theorems relating to triangulations in
HOL/Analysis/Polytope.thy but I suspect I will need to generalize and
refactor them a bit if they are to be useful for me.
For the first proof, in each step, I start with a convex polytope and want
to make a single cut that separates one of its vertices, leaving me with
two convex polytopes.
For the second proof, I want to start with an arbitrary simple polygon (not
necessarily convex), and end up with a bijection between lattice points in
the polygon and vertices in the triangulation. Here, instead of one cut
going all the way through the polygon at each step, I need to make several
small cuts as I add each new vertex to the triangulation.
Basically, I seem to need some fine grained control over how the
triangulation is performed.
1.
A “cell_complex” is a recursive data type, where each interior node
represents a (generic) cut, and each leaf represents a polytope.
2.
A “triangulation” is a subtype of “cell_complex” where each leaf is a
simplex.
3.
A “cut” is a type parameter to those type, so cuts can be hyperplanes in
one case, and lists of line segments in the other, and so other people
can
apply the idea to their own ends.
4.
A ‘ cut strategy is a function of type:: polytope => ‘cut triangulation
=> ‘cut
5.
Finally, I provide some generic function (polytope => ‘cut strategy =>
‘cut triangulation) takes care of the actual construction.
1.
Reason inductively about relationships either the polytope or the
1.
Proof 1 : Euler’s relation holds for polytopes in dimension D if it
holds in all dimensions < D and it holds for the two parts after
making a
cut [1]
2.
Proof 2: certain relationships between the numbers of edges, interior
points, and boundary points hold for the triangulation itself,
as each new
point is added. [2]
2.
I will be able to execute the algorithms on actual polytopes that I
construct in code, and produce nice little diagrams for the final paper.
I’m a programmer by trade, so I’m pretty confident in my ability to handle
part 2. I’m not so certain about part 1.
So… I think I’m basically asking for a sanity check on this approach. Does
it make sense? Are there things I should be looking at that already do
something like this? Am I going to run into trouble mixing ideas from
programming and geometry like this? Should I try to refactor the theorems
in Polytope.thy or just start from scratch?
Or is there a better way of approaching this altogether?
Thanks!
Helge Tverberg, “How to cut a convex polytope into simplices”
https://vdocuments.site/documents/how-to-cut-a-convex-
polytope-into-simplices.html
W.W. Funkenbusch, “From Euler’s Formula to Pick’s Theorem, using an Edge
Theorem”
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.
475.919&rep=rep1&type=pdf

[Manuel Eberl]

Post by José Manuel Rodriguez Caballero
This is the hard way to prove it. The easy way is to interprete Euler's
formula as a theorem in Graph Theory and then to deduce its application to
a polytope as a trivial corollary (see the book that I cited to find the
details). Dimension plays no essential role, because it is just a theorem
about a graph.

I'm not so sure about the "trivial" part. Connecting the graph-theoretic
notions of vertices, edges, and faces to the geometric ones in a formal
setting is probably not /that/ easy. In fact, it may well be the most
difficult part of the entire proof.

Manuel

[José Manuel Rodriguez Caballero]

Both Euler's formula its application to Pick's theorem are explained in a
very pedagogical way in chapter 12 of the following book:

Aigner, Martin, et al. *Proofs from the Book*. Vol. 274. Berlin: Springer,
2010. (You may find a link after a quickly search in google)

Concerning your question

Proof 1 : Euler’s relation holds for polytopes in dimension D if it

Post by Michal Wallace
holds in all dimensions < D and it holds for the two parts after
making a
cut [1] So… I think I’m basically asking for a sanity check on this
approach. Does
it make sense? Are there things I should be looking at that already do
something like this? Am I going to run into trouble mixing ideas from
programming and geometry like this?

This is the hard way to prove it. The easy way is to interprete Euler's
formula as a theorem in Graph Theory and then to deduce its application to
a polytope as a trivial corollary (see the book that I cited to find the
details). Dimension plays no essential role, because it is just a theorem
about a graph.

Concerning you observation:

I’m a programmer by trade, so I’m pretty confident in my ability to handle

Post by Michal Wallace
part 2. I’m not so certain about part 1.

In my case, I'm a mathematician by trade (Master degree), and the
programming part is what I am learning right now thanks to the people of
this mailing list. By the way, I'm open to consider any PhD position where
I can apply my mathematical skills to Isabelle or another proof assistant.

Kind Regards,
Jose M.




Message: 1

Post by Michal Wallace
Date: Sat, 11 Aug 2018 18:13:15 -0400
Subject: [isabelle] Help with Triangulation
gmail.com>
Content-Type: text/plain; charset="UTF-8"
I am working on formalizing Euler’s relation between the number of
n-dimensional faces of a polytope (aka the polyhedron formula), and then
hopefully using this to derive Pick’s theorem for the area of polygons
whose vertices fall on integer lattice points in the plane.
I intend to approach both proofs using arguments based on induction over a
triangulation.
There are a couple theorems relating to triangulations in
HOL/Analysis/Polytope.thy but I suspect I will need to generalize and
refactor them a bit if they are to be useful for me.
For the first proof, in each step, I start with a convex polytope and want
to make a single cut that separates one of its vertices, leaving me with
two convex polytopes.
For the second proof, I want to start with an arbitrary simple polygon (not
necessarily convex), and end up with a bijection between lattice points in
the polygon and vertices in the triangulation. Here, instead of one cut
going all the way through the polygon at each step, I need to make several
small cuts as I add each new vertex to the triangulation.
Basically, I seem to need some fine grained control over how the
triangulation is performed.
1.
A “cell_complex” is a recursive data type, where each interior node
represents a (generic) cut, and each leaf represents a polytope.
2.
A “triangulation” is a subtype of “cell_complex” where each leaf is a
simplex.
3.
A “cut” is a type parameter to those type, so cuts can be hyperplanes in
one case, and lists of line segments in the other, and so other people
can
apply the idea to their own ends.
4.
A ‘ cut strategy is a function of type:: polytope => ‘cut triangulation
=> ‘cut
5.
Finally, I provide some generic function (polytope => ‘cut strategy =>
‘cut triangulation) takes care of the actual construction.
1.
Reason inductively about relationships either the polytope or the
1.
Proof 1 : Euler’s relation holds for polytopes in dimension D if it
holds in all dimensions < D and it holds for the two parts after
making a
cut [1]
2.
Proof 2: certain relationships between the numbers of edges, interior
points, and boundary points hold for the triangulation itself,
as each new
point is added. [2]
2.
I will be able to execute the algorithms on actual polytopes that I
construct in code, and produce nice little diagrams for the final paper.
I’m a programmer by trade, so I’m pretty confident in my ability to handle
part 2. I’m not so certain about part 1.
So… I think I’m basically asking for a sanity check on this approach. Does
it make sense? Are there things I should be looking at that already do
something like this? Am I going to run into trouble mixing ideas from
programming and geometry like this? Should I try to refactor the theorems
in Polytope.thy or just start from scratch?
Or is there a better way of approaching this altogether?
Thanks!
Helge Tverberg, “How to cut a convex polytope into simplices”
https://vdocuments.site/documents/how-to-cut-a-convex-polyto
pe-into-simplices.html
W.W. Funkenbusch, “From Euler’s Formula to Pick’s Theorem, using an Edge
Theorem”
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.475
.919&rep=rep1&type=pdf

[José Manuel Rodriguez Caballero]

Manuel Eberl said
I'm not so sure about the "trivial" part. Connecting the graph-theoretic
notions of vertices, edges, and faces to the geometric ones in a formal
setting is probably not /that/ easy. In fact, it may well be the most
difficult part of the entire proof.

The Euler's formula that Michal needs in order to derive Pick's theorem as
a corollary is the following graph theoretic statement: V - E + F = 2 for
any connected planar graph, where V is the number of vertices, E the number
of edges and F the number of faces. Indeed, this is the approach followed
in the reference cited by Michal in his email: Funkenbusch W. W. From
Euler’s formula to Pick’s formula using an edge theorem. The American
Mathematical Monthly. 1974 Jun 1;81(6):647-8.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.475.919&rep=rep1&type=pdf

So, what Micha calls the Euler’s relation between the number of n-dimensional
faces of a polytope is not used in Funkenbusch's paper. Of course, if Micha
is interested in formalized such an n-dimensional formula anyway, he needs
to generalize my advise to dimension n, because I just sent him the
reference for n = 3, which is the only case required for proving Pick's
theorem. A claim of new proof of this result is here (I did not check it
because I do not like this approach): https://arxiv.org/pdf/1612.01271.pdf

I do not retract about my claim in the previous email: the more natural way
to prove Euler's formula is using graph theory and its generalization to
polytopes is trivial in the sense that no deep mathematical result is
needed, although you may write a little bit of code in Isabelle just to
formalize the geometric intuition. The only detail is that you need a
generalization of graph named CW-complex. Any undirected graph (loops
and/or multiple edges allowed) has a geometric realization as a
1-dimensional CW-complex.

According to Alexander Grothendieck, all your mathematical proofs become
trivial provided that you have the right definitions. It is important to
notice that the Euler characteristic of a CW-complex depends only of this
homotopy type. So, the more natural setting to formalize this theorem
should be homotopy type theory, where you do not even need real numbers
!!!!, but you can do it in Isabelle as well. Indeed, I recommend to
formalize the proof in Isabelle as follows (I'm following my own approach
with looking at any textbooks, maybe there are simpler approaches in
literature):

Step 1. You define a CW-complex in Isabelle (combinatorial/algebraic
staff). https://en.wikipedia.org/wiki/CW_complex

Step 2. You define cellular homology in Isabelle (combinatorial/algebraic
staff). https://en.wikipedia.org/wiki/Cellular_homology

Step 3. You define the Euler's characteristic as the alternated sum of the
ranks of the homology groups.

Step 4. You prove the Gauss-Bonnet theorem, either in its general form:
https://en.wikipedia.org/wiki/Gauss%E2%80%93Bonnet_theorem

or just its particular case for polytopes (due to Rene Descartes):
https://en.wikipedia.org/wiki/Angular_defect#Descartes.27_theorem

Step 5. You apply the Gauss-Bonnet theorem (or just its particular case for
polytopes) to an n-dimensional hypercube in order to show that its Euler
characteristic is 1. This computation is trivial.

Step 6. You show that any convex polytope is homeomorphic to an hypercube
of the same dimension. This is trivial too.

Step 7. In virtue of the definition of cellular homology and the result
proved in step 5, the Euler characteristic of any convex polytope is 1. We
can also say that this happens because the Euler characteristic is a
topological property, i.e., it is invariant with respect to homeomorphisms.

Step 8. You express your n-dimensional convex polytope as a CW-complex and
you apply the definition of Euler's characteristic from step 3.

Step 9. You deduce that the number of k-dimensional faces in your convex
polytope is equal to the rank of its k-th homology group. This follows from
the definition of the cellular homology.

Step 10. You obtain that the alternated sum of the k-dimensional faces of
your polytope is 1. This is the generalized Euler's formula, also named the
Euler-Poincare's formula. QED


Why the original Euler's formula involves the number 2 whereas its
generalization involves the number 1? This is because, Euler's formula, in
its original form V - E + F = 2, is not about a 3D convex polytope, but
about its surface (in the general case, we prefer to use the word boundary
in place of the word surface). Notice that we can express V - E + F = 2 as
follows:

V - E + F - T = 1,


where T = 1 is the number of 3-dimensional faces of the corresponding
CW-complex, i.e., the polytope itself.

If you watch the following video, the above mentioned results will be
easier to understand:

Also, the following book may be useful for such a formalization:
Hatcher A. Algebraic topology. 清华大学出版社有限公司; 2005.
https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

A topological formulation of Euler-Poincare's formula in terms of
CW-complexes is more useful for mathematician and physicists than the
particular case about polytopes. For example, to apply this formula to
quantum mechanics or general relativity you need the topological version,
because the space where these people are working may be non-Euclidean, but
the topological version still holds.

Good luck,
Jose M.

This is the hard way to prove it. The easy way is to interprete Euler's

Post by José Manuel Rodriguez Caballero
formula as a theorem in Graph Theory and then to deduce its application

to

Post by José Manuel Rodriguez Caballero
a polytope as a trivial corollary (see the book that I cited to find the
details). Dimension plays no essential role, because it is just a theorem
about a graph.

I'm not so sure about the "trivial" part. Connecting the graph-theoretic
notions of vertices, edges, and faces to the geometric ones in a formal
setting is probably not /that/ easy. In fact, it may well be the most
difficult part of the entire proof.
Manuel

[Michal Wallace]

Jose,

Thank you for the detailed proof outline. It's very interesting to me, and
you may well be right that it would lead to a more useful and natural
proof, but I'm afraid I'm a couple decades behind you in my mathematical
studies, and I have trouble parsing most of the words on the wikipedia
pages you link.

The highest level math course I ever took was calculus, and that was 20+
years ago. I've read various books and watched videos on different higher
math subjects along the way, but when I open (for example) your first link:
https://en.wikipedia.org/wiki/CW_complex, I'm quickly confronted with many
words I don't understand. If I look those words up, I have the same
problem. (Attaching map leads to
https://en.wikipedia.org/wiki/Adjunction_space leads to
https://en.wikipedia.org/wiki/Continuous_function#Continuous_functions_between_topological_spaces
leads to https://en.wikipedia.org/wiki/Ball_(mathematics) (which I skipped
over back on the CW page, thinking I probably knew what it meant, but now
I'm not sure, and so on and so on.)

That isn't to say that I'm a big dummy head and could never understand any
of this. :) Just about everywhere one looks in math and programming, one
finds these big complicated graphs of ideas that have to be explored in
order to get anything done. It's easy to get lost.

Currently, I'm also pretty lost when it comes to Isabelle. As a software
developer, I've dealt with this many times: I'm encountering a new code
base which seems tangled and complicated. Presumably it was all small and
simple at one point (maybe way back when the first LCF prototypes were
made) and now, many years of ideas and improvements and probably false
starts are scattered everywhere. (For example, Larry ported Polytope.thy
(and the triangulation stuff in it) from HOL-Light, and the author of
HOL-Light has since added proofs for both the polyhedron formula and pick's
theorem, and both of those proofs re-implement their own separate take on
triangulation.

Unfortunately, HOL-Light lacks a nice syntax like Isar, so for me to port
those proofs directly would require learning a whole lot about
HOL-Light.... That might be fun, too, but there's only so many rabbit holes
one can go down at once. :)

In any case, I can get my head around Triangulations, and I can see a
pretty clear path from what I've proved so far, to proving Pick's theorem
and the polyhedron formula, and the only thing I have to focus on learning
is "how to express my ideas in Isabelle"... which is the main thing I want
to learn right now.

My hope is that when I'm done, I'll be able to publish my proof as a paper
that a pretty wide audience can understand, which not only proves some
things about polyhedra, but also shows other programmers who might be
interested a thing or two about Isabelle and why it's neat, and maybe even
shows some math folks how you can use Isabelle to write proofs that are not
only human readable and computer checked, but also directly executable.

More importantly, my hope is that when I'm done, I'll be a little better at
proving things in Isabelle, so that maybe the next time I formalize
something, I can focus more on learning new math. When I get there, I might
just take another look at your outline here, and see how far I can get
along the path you laid out. (I'd certainly be curious to compare the two
approaches in the end.)





On Tue, Aug 14, 2018 at 4:15 AM José Manuel Rodriguez Caballero <

Manuel Eberl said

Post by Manuel Eberl
I'm not so sure about the "trivial" part. Connecting the graph-theoretic
notions of vertices, edges, and faces to the geometric ones in a formal
setting is probably not /that/ easy. In fact, it may well be the most
difficult part of the entire proof.

The Euler's formula that Michal needs in order to derive Pick's theorem as
a corollary is the following graph theoretic statement: V - E + F = 2 for
any connected planar graph, where V is the number of vertices, E the number
of edges and F the number of faces. Indeed, this is the approach followed
in the reference cited by Michal in his email: Funkenbusch W. W. From
Euler’s formula to Pick’s formula using an edge theorem. The American
Mathematical Monthly. 1974 Jun 1;81(6):647-8.
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.475.919&rep=rep1&type=pdf
So, what Micha calls the Euler’s relation between the number of n-dimensional
faces of a polytope is not used in Funkenbusch's paper. Of course, if
Micha is interested in formalized such an n-dimensional formula anyway, he
needs to generalize my advise to dimension n, because I just sent him the
reference for n = 3, which is the only case required for proving Pick's
theorem. A claim of new proof of this result is here (I did not check it
because I do not like this approach): https://arxiv.org/pdf/1612.01271.pdf
I do not retract about my claim in the previous email: the more natural
way to prove Euler's formula is using graph theory and its generalization
to polytopes is trivial in the sense that no deep mathematical result is
needed, although you may write a little bit of code in Isabelle just to
formalize the geometric intuition. The only detail is that you need a
generalization of graph named CW-complex. Any undirected graph (loops
and/or multiple edges allowed) has a geometric realization as a
1-dimensional CW-complex.
According to Alexander Grothendieck, all your mathematical proofs become
trivial provided that you have the right definitions. It is important to
notice that the Euler characteristic of a CW-complex depends only of this
homotopy type. So, the more natural setting to formalize this theorem
should be homotopy type theory, where you do not even need real numbers
!!!!, but you can do it in Isabelle as well. Indeed, I recommend to
formalize the proof in Isabelle as follows (I'm following my own approach
with looking at any textbooks, maybe there are simpler approaches in
Step 1. You define a CW-complex in Isabelle (combinatorial/algebraic
staff). https://en.wikipedia.org/wiki/CW_complex
Step 2. You define cellular homology in Isabelle (combinatorial/algebraic
staff). https://en.wikipedia.org/wiki/Cellular_homology
Step 3. You define the Euler's characteristic as the alternated sum of the
ranks of the homology groups.
https://en.wikipedia.org/wiki/Gauss%E2%80%93Bonnet_theorem
https://en.wikipedia.org/wiki/Angular_defect#Descartes.27_theorem
Step 5. You apply the Gauss-Bonnet theorem (or just its particular case
for polytopes) to an n-dimensional hypercube in order to show that its
Euler characteristic is 1. This computation is trivial.
Step 6. You show that any convex polytope is homeomorphic to an hypercube
of the same dimension. This is trivial too.
Step 7. In virtue of the definition of cellular homology and the result
proved in step 5, the Euler characteristic of any convex polytope is 1. We
can also say that this happens because the Euler characteristic is a
topological property, i.e., it is invariant with respect to homeomorphisms.
Step 8. You express your n-dimensional convex polytope as a CW-complex and
you apply the definition of Euler's characteristic from step 3.
Step 9. You deduce that the number of k-dimensional faces in your convex
polytope is equal to the rank of its k-th homology group. This follows
from the definition of the cellular homology.
Step 10. You obtain that the alternated sum of the k-dimensional faces of
your polytope is 1. This is the generalized Euler's formula, also named the
Euler-Poincare's formula. QED
Why the original Euler's formula involves the number 2 whereas its
generalization involves the number 1? This is because, Euler's formula, in
its original form V - E + F = 2, is not about a 3D convex polytope, but
about its surface (in the general case, we prefer to use the word boundary
in place of the word surface). Notice that we can express V - E + F = 2
V - E + F - T = 1,
where T = 1 is the number of 3-dimensional faces of the corresponding
CW-complex, i.e., the polytope itself.
If you watch the following video, the above mentioned results will be
easier to understand: http://youtu.be/1wtq5A7VMsA
Hatcher A. Algebraic topology. 清华大学出版社有限公司; 2005.
https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
A topological formulation of Euler-Poincare's formula in terms of
CW-complexes is more useful for mathematician and physicists than the
particular case about polytopes. For example, to apply this formula to
quantum mechanics or general relativity you need the topological version,
because the space where these people are working may be non-Euclidean, but
the topological version still holds.
Good luck,
Jose M.

Post by Manuel Eberl
This is the hard way to prove it. The easy way is to interprete Euler's

Post by José Manuel Rodriguez Caballero
formula as a theorem in Graph Theory and then to deduce its application

to

Post by José Manuel Rodriguez Caballero
a polytope as a trivial corollary (see the book that I cited to find the
details). Dimension plays no essential role, because it is just a

theorem

Post by José Manuel Rodriguez Caballero
about a graph.

I'm not so sure about the "trivial" part. Connecting the graph-theoretic
notions of vertices, edges, and faces to the geometric ones in a formal
setting is probably not /that/ easy. In fact, it may well be the most
difficult part of the entire proof.
Manuel

[Jeremy Dawson]

Post by Michal Wallace
Unfortunately, HOL-Light lacks a nice syntax like Isar, so for me to port
those proofs directly would require learning a whole lot about
HOL-Light.... That might be fun, too, but there's only so many rabbit holes
one can go down at once.:)

Hi Michal,

Isar may be a nice syntax, in the sense that you can look at a page of
it and not see many semicolons or parentheses or square brackets, but
it's not nice otherwise. Just like English text would be nicer without
any punctuation. You have to learn to understand the page of text.

With HOL Light, I understand it is written in O'Caml, which is a
sensibly designed and well-documented language. And I assume HOL Light
is also well documented - if it's not, then choose HOL4, which is.

Post by Michal Wallace
My hope is that when I'm done, I'll be able to publish my proof as a paper
that a pretty wide audience can understand, which not only proves some
things about polyhedra, but also shows other programmers who might be
interested a thing or two about Isabelle and why it's neat, and maybe even
shows some math folks how you can use Isabelle to write proofs that are not
only human readable and computer checked, but also directly executable.

Forget that. No-one will want to read a proof document that includes
every step that the computer needs to complete its proof.

I don't say there aren't exceptions, but do your readers the courtesy of
writing a document for them which explains the proof in the level of
detail they need. Mostly the computer uses far more detailed steps,
which the reader won't want. (Unless he/she really does want to check
the computer has done it right). Of course this may vary between
fields, but I've had to write proofs which involved tens of thousands of
elementary steps.

Which means that a proof in HOL Light or HOL4 or Coq (usually structured
with more rather than fewer intermediate lemmas) will be what the reader
wants.

And of course you may be interested in whether your computer-based
proofs will still run in 10 or 20 years' time.

Hope this gives you food for thought.

Cheers,

Jeremy

[Lawrence Paulson]

Jeremy, I think you're quite missing the point about the difference between Isar and ML. It's not about whether the syntax is pretty or not or how much punctuation it requires. It is that an Isar proof presents the user with a structured outline of the argument including intermediate assertions, while a more traditional ML proof is a computer program that generates the required result but is completely opaque about the mathematical argument itself. One can look at a long Isar proof and follow the argument without using a computer, which is completely impossible in the case of a long proof coded in ML.

As for whether the proof will run in 20 years' time: it's interesting to compare the differences between successive versions of the libraries in HOL Light or Coq compared with Isabelle. We are constantly streamlining our proofs and even changing definitions, because we can: any errors are immediately flagged in exactly the critical place. With those other systems, a proof once written is almost never changed, unless it is replaced by an entirely new proof. That's how we have managed to keep the 2 million lines of proofs in the AFP working since 2004.

Larry

Post by Jeremy Dawson

Post by Michal Wallace
Unfortunately, HOL-Light lacks a nice syntax like Isar, so for me to port
those proofs directly would require learning a whole lot about
HOL-Light.... That might be fun, too, but there's only so many rabbit holes
one can go down at once.:)

Hi Michal,
Isar may be a nice syntax, in the sense that you can look at a page of it and not see many semicolons or parentheses or square brackets, but it's not nice otherwise. Just like English text would be nicer without any punctuation. You have to learn to understand the page of text.
With HOL Light, I understand it is written in O'Caml, which is a sensibly designed and well-documented language. And I assume HOL Light is also well documented - if it's not, then choose HOL4, which is.

Post by Michal Wallace
My hope is that when I'm done, I'll be able to publish my proof as a paper
that a pretty wide audience can understand, which not only proves some
things about polyhedra, but also shows other programmers who might be
interested a thing or two about Isabelle and why it's neat, and maybe even
shows some math folks how you can use Isabelle to write proofs that are not
only human readable and computer checked, but also directly executable.

Forget that. No-one will want to read a proof document that includes every step that the computer needs to complete its proof.
I don't say there aren't exceptions, but do your readers the courtesy of writing a document for them which explains the proof in the level of detail they need. Mostly the computer uses far more detailed steps, which the reader won't want. (Unless he/she really does want to check the computer has done it right). Of course this may vary between fields, but I've had to write proofs which involved tens of thousands of elementary steps.
Which means that a proof in HOL Light or HOL4 or Coq (usually structured with more rather than fewer intermediate lemmas) will be what the reader wants.
And of course you may be interested in whether your computer-based proofs will still run in 10 or 20 years' time.
Hope this gives you food for thought.
Cheers,
Jeremy

[Jeremy Dawson]

Hi Larry,

I don't think so - my remark about pretty syntax was purely a response
to what was said about pretty syntax.

I understand that Isar is meant to produce readable proofs. I
questioned whether it achieves this, because
(1) they're (in many cases) too long and detailed to read
(2) the meaning of many of the words in Isar is totally obscure to
someone who has only the documentation to rely on (and for those that
aren't totally obscure, it's because they're analogous to things
explained in the earlier documentation, which unfortunately seems to
have now been abandoned - and which I believe you wrote, so I should
thank you wholeheartedly for that)

As a matter of fact I've wondered whether the increased readability of
Isar proofs is mainly because the text of intermediate steps gets
included in the text of the document - ie, if one did a proof in ML with
extensive use of subgoal_tac, whether it would be just as good as an
Isar proof.

Of course this is all quite irrelevant in the case of a proof like one I
once had which had I think over 60000 elementary steps (ie, uses of
rtac, etac, atac etc) which no-one is ever going to write or read in ML
Isar or anything else. What no-one has ever been willing to tell me is
how Isar aficionados handle this sort of proof.

Sorry for the length of this - but I do understand the concept of
readable proofs.

Cheers,

Jeremy

Post by Lawrence Paulson
Jeremy, I think you're quite missing the point about the difference between Isar and ML. It's not about whether the syntax is pretty or not or how much punctuation it requires. It is that an Isar proof presents the user with a structured outline of the argument including intermediate assertions, while a more traditional ML proof is a computer program that generates the required result but is completely opaque about the mathematical argument itself. One can look at a long Isar proof and follow the argument without using a computer, which is completely impossible in the case of a long proof coded in ML.

[Michal Wallace]

Isar's syntax enables readable proofs, but it doesn't ensure that proofs
are readable.
That requires a lot of work on the part of the author, including:

- picking clear names/notation
- breaking proofs down into smaller, easier to understand parts
- adding text, comments and section headers

It's certainly true that in many cases, this work has not been done. The
file I've been working with the most:

https://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Polytope.html

is essentially a port of:

https://github.com/jrh13/hol-light/blob/master/Multivariate/polytope.ml

The two have diverged a bit, but at one point there was a one-to-one
mapping between the lemmas, and while the Isabelle
version is still very very dense and nearly comment-free, it's (at least to
me) far more readable than the original.

OTOH, I found the latest entry to the AFP to be extremely readable:

https://www.isa-afp.org/entries/Minsky_Machines.html

Most of the lemmas are short, and pretty much all of them are explained in
prose up front.

As for your 60000 elementary steps....

Some people actually do want that. One thing that draws people to
metamath.org,
for example, is that every single step is shown... The only rules are
syntax definition and substitution, and the people that
like metamath consider that an extremely important feature. On the other
hand, they have the good taste to break each
proof down into small chunks, so you rarely (?) see a proof that's more
than a screenful of text.

I suppose if I were confronted with a proof that long in Isabelle, and I
knew many of the steps could be automated, I
would probably start breaking off little chunks at the start or end of the
proof into their own lemmas, or
possibly try to pick out useful mid-steps and try to get sledgehammer to
replace chunks in the middle.

(Well, okay... with 60,000 lines, I would probably write a program that
would attempt to do this for me...)

I have a smaller but similar problem in front of me right now: over in
HOL-Analysis.Polytope.thy,
there's a lemma that's 459 lines long (simplicial_subdivision_aux), and I
have to decide between
trying to understand it and then refactoring it, or just trying to start
from scratch.

I haven't made up my mind yet, but even as big and complicated as it seems
to me, the code folding,
ability to inspect the proof state at each point, and the ability to
ctrl-click on any word to see its definition
certainly make it seem much more approachable even without someone to guide
me through it.

You seem to be feeling a lot of frustration with Isabelle. I can't say I'm
not feeling similar frustrations, but
in my experience, that frustration is just a thing that happens when you
try to really understand any
big complicated system. The way through it is to be patient, ask questions,
experiment, study what
other people have done (or what other people have *asked*, either here or
on stack overflow), and
just trust that eventually things that were confusing at first will
eventually start to make sense.

Also... My impression (and I could be wrong about this) is that most of the
users of Isabelle are not just
going it alone, but are academics working closely with and being taught by
other people who are
intimately familiar with the system already. Nobody's written a "Learn You
an Isar for Great Good" and
there's not (yet) been a huge influx of curious outsiders blazing trails
for everyone else. So that
means people like you and me (who seem to be sometimes frustrated
outsiders) have on opportunity
to be the trailblazers -- the ones who subject ourselves to getting lost
for a while, knowing
that when we eventually do find our way, we can make it easier for the next
person.

I can see that sounding pretty trite/condescending, and if so, sorry...
It's just an attitude that I
find keeps me sane and cheerful whenever I have to deal with new and often
overwhelming complexity. :)

Post by Jeremy Dawson
Hi Larry,
I don't think so - my remark about pretty syntax was purely a response
to what was said about pretty syntax.
I understand that Isar is meant to produce readable proofs. I
questioned whether it achieves this, because
(1) they're (in many cases) too long and detailed to read
(2) the meaning of many of the words in Isar is totally obscure to
someone who has only the documentation to rely on (and for those that
aren't totally obscure, it's because they're analogous to things
explained in the earlier documentation, which unfortunately seems to
have now been abandoned - and which I believe you wrote, so I should
thank you wholeheartedly for that)
As a matter of fact I've wondered whether the increased readability of
Isar proofs is mainly because the text of intermediate steps gets
included in the text of the document - ie, if one did a proof in ML with
extensive use of subgoal_tac, whether it would be just as good as an
Isar proof.
Of course this is all quite irrelevant in the case of a proof like one I
once had which had I think over 60000 elementary steps (ie, uses of
rtac, etac, atac etc) which no-one is ever going to write or read in ML
Isar or anything else. What no-one has ever been willing to tell me is
how Isar aficionados handle this sort of proof.
Sorry for the length of this - but I do understand the concept of
readable proofs.
Cheers,
Jeremy

Post by Lawrence Paulson
Jeremy, I think you're quite missing the point about the difference

between Isar and ML. It's not about whether the syntax is pretty or not or
how much punctuation it requires. It is that an Isar proof presents the
user with a structured outline of the argument including intermediate
assertions, while a more traditional ML proof is a computer program that
generates the required result but is completely opaque about the
mathematical argument itself. One can look at a long Isar proof and follow
the argument without using a computer, which is completely impossible in
the case of a long proof coded in ML.

[Ken Kubota]

Post by Michal Wallace
for your 60000 elementary steps....
Some people actually do want that. One thing that draws people to
metamath.org,
for example, is that every single step is shown... The only rules are
syntax definition and substitution, and the people that
like metamath consider that an extremely important feature. On the other
hand, they have the good taste to break each
proof down into small chunks, so you rarely (?) see a proof that's more
than a screenful of text.

It would be desirable to have a mode in Isabelle in which for an automated proof
each single step is made explicit and displayed afterwards (or saved to disk in a file)
with full type information.
It shouldn't be too difficult to implement both modes, one without tracking
(for performance), and one with tracking (allowing one to follow each single
step).

Post by Michal Wallace
You seem to be feeling a lot of frustration with Isabelle. I can't say I'm
not feeling similar frustrations, but
in my experience, that frustration is just a thing that happens when you
try to really understand any
big complicated system. The way through it is to be patient, ask questions,
experiment, study what
other people have done (or what other people have *asked*, either here or
on stack overflow), and
just trust that eventually things that were confusing at first will
eventually start to make sense.

This isn't the case for HOL (HOL4). With the HOL handbook [Gordon and Melham, 1993]
(and an online tutorial) I was able to fully understand and work with the system
within 24 hours.

Generally speaking, with a clear and concise presentation of the concepts and the logic(s)
within a good documentation (and not many scattered papers) the principles of any large
system can be explained properly.

Maybe the Isabelle team should consider asking Andy Pitts to write a logic part
for Isabelle and Isabelle/HOL (as soon as no major changes are expected anymore)
with the same brilliance like that of the logic part of the HOL handbook.

Post by Michal Wallace
Also... My impression (and I could be wrong about this) is that most of the
users of Isabelle are not just
going it alone, but are academics working closely with and being taught by
other people who are
intimately familiar with the system already. Nobody's written a "Learn You
an Isar for Great Good" and
there's not (yet) been a huge influx of curious outsiders blazing trails
for everyone else. So that
means people like you and me (who seem to be sometimes frustrated
outsiders) have on opportunity
to be the trailblazers -- the ones who subject ourselves to getting lost
for a while, knowing
that when we eventually do find our way, we can make it easier for the next
person.

This is exactly what I wrote some time ago on this list (concerning Isabelle,
not just Isar).

The theoretical foundation ([Paulson, 1988]) is excellent, and Isabelle is an
impressive software, but the documentation is a nightmare. In it, logical
foundations are mixed up with technical details. It has many references
to articles outside of the documentation (at least in earlier versions), forcing
one to struggle one's way through a jungle of numerous articles. I believe
it took me years just to find out that [Paulson, 1988] is the theoretical foundation.

The documentation should enable one to work with the software independently,
but in fact it is a supplementary reference for "academics working closely with
and being taught by other people who are intimately familiar with the system
already".


For references, please see: http://doi.org/10.4444/100.111

____________________________________________________

Ken Kubota
http://doi.org/10.4444/100

[Makarius]

Post by Jeremy Dawson
Which means that a proof in HOL Light or HOL4 or Coq (usually structured
with more rather than fewer intermediate lemmas) will be what the reader
wants.
And of course you may be interested in whether your computer-based
proofs will still run in 10 or 20 years' time.

I must emphasize that the isabelle-users mailing list is for current
Isabelle releases (e.g. Isabelle2018, Isabelle2017, Isabelle2016), but
not 20-30 years back in time as these attitudes suggest.

The Archive of Formal Proofs is the practical proof that we managed to
address certain problems of proof composition and maintenance from the
past. From there we should continue to move forwards, not backwards to
nostalgic ML "proof scripts".

Users who do like that old style are invited to use HOL Light or HOL4:
they are fine systems with their own mailing list.


Makarius

[Lars Hupel]

Post by Jeremy Dawson
And of course you may be interested in whether your computer-based
proofs will still run in 10 or 20 years' time.

Luckily, the AFP has a track record of 14 years continuous maintenance
of formal material.

Cheers
Lars

[Jeremy Dawson]

Post by Lars Hupel

Post by Jeremy Dawson
And of course you may be interested in whether your computer-based
proofs will still run in 10 or 20 years' time.

Luckily, the AFP has a track record of 14 years continuous maintenance
of formal material.
Cheers
Lars

I accept that. My remark was prompted by the attitude of the "owners"
of Isabelle to proofs dating from earlier than 14 years ago.
(To be fair, this is no doubt attributable to the "owners" of Isabelle
14 years ago than to the "owners" of Isabelle now).

Obviously the concern would be that the same attitudes resurface.

Cheers,

Jeremy

[Lars Hupel]

Post by Jeremy Dawson
I accept that. My remark was prompted by the attitude of the "owners"
of Isabelle to proofs dating from earlier than 14 years ago.
(To be fair, this is no doubt attributable to the "owners" of Isabelle
14 years ago than to the "owners" of Isabelle now).
Obviously the concern would be that the same attitudes resurface.

The maintenance situation in Isabelle is way ahead of other
sub-disciplines in computer science. If you insist on nothing to change
ever, you'll get stasis.

(Relatedly, I really don't like the insinuation that Isabelle developers
don't care about old things, because that's very much not the case.)

[Jeremy Dawson]

Post by Lars Hupel

I accept that.  My remark was prompted by the attitude of the "owners"
of Isabelle to proofs dating from earlier than 14 years ago.
(To be fair, this is no doubt attributable to the "owners" of Isabelle
14 years ago than to the "owners" of Isabelle now).
Obviously the concern would be that the same attitudes resurface.

The maintenance situation in Isabelle is way ahead of other
sub-disciplines in computer science. If you insist on nothing to change
ever, you'll get stasis.

Hi Lars,

No I don't insist on that. Backward compatibility is what the situation
calls for. Like how you can read 15-year old pdf documents.

Post by Lars Hupel
(Relatedly, I really don't like the insinuation that Isabelle developers
don't care about old things, because that's very much not the case.)

I actually know something about this - all my Isabelle proofs work with
Isabelle 2005 or earlier (because they are (almost) all from before
then, build upon work from before then, or are an adaptation of work
from before then). Makarius Wenzel suggested I rewrite the lot. Not
suprisingly, that is not what I'm paid to do.

Cheers,

Jeremy

[Lars Hupel]

No I don't insist on that.  Backward compatibility is what the situation
calls for.  Like how you can read 15-year old pdf documents.

Apples and oranges. PDF is a standardized format with significant
industry buy-in. Isar isn't.

(Apart from that, you can also still read Isabelle proof documents. You
just can't change them easily. Incidentally, the same situation as for
PDFs.)

I actually know something about this - all my Isabelle proofs work with
Isabelle 2005 or earlier (because they are (almost) all from before
then, build upon work from before then, or are an adaptation of work
from before then).  Makarius Wenzel suggested I rewrite the lot. Not
suprisingly, that is not what I'm paid to do.

Same argument applies. People developing Isabelle are not paid to
maintain 100% backwards compatibility.

[José Manuel Rodriguez Caballero]

Post by Jeremy Dawson
Sorry for the length of this - but I do understand the concept of
readable proofs.

My answer will be according to my personal experience and it may be
different from the conventional definition of readable proofs.

In January of this year, I began to learn Coq and I gave the impression
that it was a sort of video-game: it is very hard to understand a proof in
Coq from a printed page of it, you need a computer to reproduce it step by
step. When I learned Isabelle from the manuals (it take me almost week), I
gave the impression that I was reading an ordinary text book in
mathematics. So, a readable proof is for me a proof which follow the same
structure as a traditional mathematical proof from a textbook, e.g., e.g.,
Algebra by Serge Lang.

Post by Jeremy Dawson
I understand that Isar is meant to produce readable proofs. I
questioned whether it achieves this, because
(1) they're (in many cases) too long and detailed to read
(2) the meaning of many of the words in Isar is totally obscure to
someone who has only the documentation to rely on (and for those that
aren't totally obscure, it's because they're analogous to things
explained in the earlier documentation, which unfortunately seems to
have now been abandoned - and which I believe you wrote, so I should
thank you wholeheartedly for that)

Concerning (1), what I do is to read just the more interesting parts, like
in any text-book of mathematics. The journal of American Mathematical
Monthly rejected me a manuscript because it was too long and detailed to
read:

The Editor wrote: we do not think that the *Monthly* is the right place for

Post by Jeremy Dawson
this manuscript; the paper is a dense read and it is unlikely that the
typically *Monthly* reader will follow the paper most of the way through.
There are thirteen lemmas required to get to the main result, and this does
not seem appropriate for a *Monthly* article, which should be a friendly
read and even appealing to non-specialists. The paper appears to represent
good work, but we suggest that it be submitted instead to a standard
research journal.

So, if someone formalize my paper, it will be unreadable in Isar in the
sense (1), because my original approach was like that. The solution to (1)
does not belong to computer science, but to mathematics: the need for a
simpler proof. This was what I did in another paper, which was published in
Journal of Number Theory, because I obtained the same result in a simpler
way, using another mathematical approach to the same problem.

Concerning (2), I do not see Isar as obscure and I learned Isar just from
the documentation. If the people which will use Isabelle/Isar are
mathematician, they read even more obscure papers every day. As
mathematician (I have a Master degree), to learn Isabelle was easier than
to learn any course of pure mathematics.

If a mathematical proof in a textbook is readable and its formalization in
Isar is not readable, the problem is not Isar, but the person who
formalized that proof. Sometimes this happens when people formalizing a
proof in Isabelle do not have a global idea of the theory that they are
formalizing. This is the reason why multi-disciplinary collaboration is
important in this field. In particular, some theorems can be proved in
several ways and the person who is formalizing this theorem, because of
lack of knowledge, choose the less readable way.

For example, if you wants to formalize the proof of the prime number
theorem, you have two options: either you use elementary number theory
(Erdos-Selberg's approach), which is unreadable in the sense of (1) or you
use complex analysis (Hadamard - de la Vallee Poussin's approach), which is
readable in the sense of (1).

Kind Regards,
Jose M.

[Jeremy Dawson]

Post by José Manuel Rodriguez Caballero
Concerning (2), I do not see Isar as obscure and I learned Isar just
from the documentation. If the people which will use Isabelle/Isar are
mathematician, they read even more obscure papers every day.

Well, there are different sort of "obscurity". I guess you will have
heard of a certain style of mathematical proof described,
contemptuously, as "handwaving". Is a "handwaving" proof, not
containing a single mathematical symbol, more or less "obscure" than a
proper proof? (That's a rhetorical question).

As

Post by José Manuel Rodriguez Caballero
mathematician (I have a Master degree), to learn Isabelle was easier
than to learn any course of pure mathematics.

Great. But my experience is that it's at least ten times harder than
HOL4 or the old Isabelle, or Coq (with the caveat I know only a small
amount of using Coq). And what's most noteworthy is that lots of people
will spend a lot of time replying to my posts, but they will never
answer questions about what Isar commands actually do to the state of a
partly completed proof.

Cheers,

Jeremy

[José Manuel Rodriguez Caballero]

Post by Michal Wallace
Also... My impression (and I could be wrong about this) is that most of the
users of Isabelle are not just
going it alone, but are academics working closely with and being taught by
other people who are
intimately familiar with the system already. Nobody's written a "Learn You
an Isar for Great Good" and
there's not (yet) been a huge influx of curious outsiders blazing trails
for everyone else.

Another motivation to learn Isar for an outsider is to avoid the authority
fallacy and to discover by oneself his mistakes if there are any. Indeed, I
know someone who claimed a solution of many mathematical open problems,
including the Riemann Hypothesis and the experts did not read his papers,
because they assumed that the author was wrong. My advice to him was this:
try to formalize your proof in Isar and if you succeed, all mathematicians
will take you seriously. Here is the link to the claim of solution of the
Riemann Hypothesis (I did not read this paper for the same reason that I am
criticizing): https://arxiv.org/pdf/1804.04700.pdf

In the case of the young Norwegian genius Niels Abel, who discovered that
the 5th equation cannot be solved in radicals, when he sent his proof to
Gauss, who was very famous at that time, laughing, Gauss did not read it,
thinking that Niels Abel was just another crank.

Post by Michal Wallace
So that
means people like you and me (who seem to be sometimes frustrated
outsiders) have on opportunity
to be the trailblazers -- the ones who subject ourselves to getting lost
for a while, knowing
that when we eventually do find our way, we can make it easier for the next
person.

In my case, although I am an outsider in the sense that I had not the
opportunity to work in Isabelle in an academic program yet, I do not feel
frustrated with Isabelle. On the contrary, I think that Isabelle is very
easy to learn and very practical in order to formally verify my own
mathematical results before publication. In that way, the reviewing process
in the journal is quickly.

I do not think that people using Isar are a kind of trailblazers, because
Isar is just a formalization of the traditional way to write in
mathematics. Since Euclid, mathematicians are doing Isar, maybe with other
words (in written in Ancient Greek). If you want to be a trailblazer in the
way people do mathematics, write a code in UniMath, which is a revolution
in mathematics: https://github.com/UniMath/UniMath

As I already said, one of my dreams is that Isabelle will use homotopy type
theory someday, because the homotopy type theory in Coq lacks something so
fundamental as Isar.


Kind Regards,
Jose M.