4 ms·

Formalizing the H-Principle and Sphere Eversion

23 points by ykonstant 4y ago

ykonstant 4y ago
This paper uses the Lean 3 language to formalize the proof of an important theorem in differential topology. Geometric arguments are notoriously difficult to formalize due to their non-symbolic nature and sometimes vague exposition; this work demonstrates (among other things) that even topics involving infinitesimal geometric reasoning in high dimensions with imprecise language can be formalized. Fascinatingly, the paper further provides humanly usable elaboration of many vague arguments geometers and analysts use (for instance, using filters to formalize nearness arguments). To me this is an under-rated aspect of formalization: it has the potential to clarify our own, human to human communication of human proofs.
- ogogmad 4y ago
  The way filters are explained is interesting: The intuition is similar to Non-Standard Analysis, and indeed models of NSA are constructed using a type of filter. I somehow think NSA is more "user friendly". Would anybody contradict? I recall a ring-theorist's way of looking at filters is: The filters in a Boolean algebra B are obtained by forming the Boolean algebra B^* dual to B, forming the Boolean ring corresponding to B^*, and then taking its ideals. Alternatively, a filter over a Boolean algebra B is just some homomorphism f:B^* -> {0,1} where {0,1} is the two-element Boolean algebra.
  - yuppiemephisto 4y ago
    I have pretty extensive experience with nonstandard analysis and you’re right. It’s just way easier to use nonstandard analysis since we have so many intuitions for plain numbers, and the construction works in every structure.
  - ykonstant 4y ago
    I have no experience with NSA so I cannot comment on its merits, but I have heard rumors that some analysts and ergodic theorists like "thinking in it" for certain problems in infinite combinatorics. Now, filters and ultrafilters are now extensively used in ergodic theory and probability to "soften" tricky analytic arguments; they have proven especially fruitful for tackling problems in combinatorics and Ramsey theory. Vitali Bergelson is a big proponent of their use, and recently Moreira, Richter and Robertson proved a fundamental result [0] in that style. For me, the most intuitive way of thinking about filters is as measure 1 sets in a (finitely additive) probability space. Their basic properties then become very clear. Principal ultrafilters, for instance, correspond to delta masses at individual points. As a little challenge, try to find "a programmer's way" of thinking about filters and ultrafilters. [0] https://annals.math.princeton.edu/2019/189-2/p04 https://annals.math.princeton.edu/2019/189-2/p04
    - 082349872349872 4y ago
      > As a little challenge, try to find "a programmer's way" of thinking about filters and ultrafilters. As a programmer attempting to develop an intuition for filters, are the following at all close? - a filter is a funny kind of predicate (involving order shenanigans) - an ultrafilter is a classical predicate, with excluded middle.
      - ykonstant 4y ago
        Very good; your insight in your second observation in particular is excellent. But you can push the first observation much further. I will let other people think about it too before giving my own thoughts.
  - kmill 4y ago
    I can't really compare non-standard analysis with filters due to not knowing much about NSA, but filters are a natural sort of completion of the poset of subsets, the pro-completion. Every subset can be naturally regarded as a filter (a principal filter), and I think of filters in general are sort of "thick" sets -- sets with some sort of infinitesimal fringe. There's also a helpful coincidence that open filters (filters on the poset of open subsets of a topological space) can be perfectly represented as filters. It makes sense to work with "functions" whose domains and ranges are filters. From this perspective, a function X -> Y is continuous at x if it can be restricted to be a function nbhd x -> nbhd f(x), where nbhd x denotes the principal open filter from all the open neighborhoods of x. If you're familiar with the germ at x of a smooth function f : X -> R, this is exactly the same concept as the restriction of f to a function nbhd x -> R. It's also possible to restrict to a germ at any given subset of f, which I think is neat. For example, you can restrict a smooth function to an infinitesimal neighborhood of a smooth submanifold. These are some of the reasons why I think that filters have some "user friendliness," once you get a feel for them.
defrost 4y ago
For those curious, the paper is about formal manipulation (computers!) in mathematical proof in the domain of geometric topology where a lot of hand waving (err, sorry, intuition) can go down. The result this is applied to is one by Smale (of the Horseshoe Map and other notions) that a sphere (ie abstract basketball 2D surface in 3 space) can be turned inside out without puncturing or creasing. Here's a 20 minute video that starts with an outline of the problem and then discusses approaches. https://www.youtube.com/watch?v=OI-To1eUtuU https://www.youtube.com/watch?v=OI-To1eUtuU This also may interest some: https://www.researchgate.net/publication/7942052_Visualizing_a_sphere_eversion https://www.researchgate.net/publication/7942052_Visualizing...
- RBerenguel 4y ago
  The co-author of the article linked has a very "fun" book on how to better draw on whiteboards, particularly for topology: https://link.springer.com/book/10.1007/978-0-387-68120-7 https://link.springer.com/book/10.1007/978-0-387-68120-7 His main example in the book is showcasing the sphere eversion.
kmill 4y ago
Here's the website where they kept track of the status of the Sphere Eversion Project: https://leanprover-community.github.io/sphere-eversion/ https://leanprover-community.github.io/sphere-eversion/ They have a dependency graph that shows the general structure of the argument: https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph_document.html https://leanprover-community.github.io/sphere-eversion/bluep...

23 points by ykonstant 4y ago

This paper uses the Lean 3 language to formalize the proof of an important theorem in differential topology. Geometric arguments are notoriously difficult to formalize due to their non-symbolic nature and sometimes vague exposition; this work demonstrates (among other things) that even topics involving infinitesimal geometric reasoning in high dimensions with imprecise language can be formalized. Fascinatingly, the paper further provides humanly usable elaboration of many vague arguments geometers and analysts use (for instance, using filters to formalize nearness arguments). To me this is an under-rated aspect of formalization: it has the potential to clarify our own, human to human communication of human proofs.

ogogmad 4y ago
The way filters are explained is interesting: The intuition is similar to Non-Standard Analysis, and indeed models of NSA are constructed using a type of filter. I somehow think NSA is more "user friendly". Would anybody contradict? I recall a ring-theorist's way of looking at filters is: The filters in a Boolean algebra B are obtained by forming the Boolean algebra B^* dual to B, forming the Boolean ring corresponding to B^*, and then taking its ideals. Alternatively, a filter over a Boolean algebra B is just some homomorphism f:B^* -> {0,1} where {0,1} is the two-element Boolean algebra.
- yuppiemephisto 4y ago
  I have pretty extensive experience with nonstandard analysis and you’re right. It’s just way easier to use nonstandard analysis since we have so many intuitions for plain numbers, and the construction works in every structure.
- ykonstant 4y ago
  I have no experience with NSA so I cannot comment on its merits, but I have heard rumors that some analysts and ergodic theorists like "thinking in it" for certain problems in infinite combinatorics. Now, filters and ultrafilters are now extensively used in ergodic theory and probability to "soften" tricky analytic arguments; they have proven especially fruitful for tackling problems in combinatorics and Ramsey theory. Vitali Bergelson is a big proponent of their use, and recently Moreira, Richter and Robertson proved a fundamental result [0] in that style. For me, the most intuitive way of thinking about filters is as measure 1 sets in a (finitely additive) probability space. Their basic properties then become very clear. Principal ultrafilters, for instance, correspond to delta masses at individual points. As a little challenge, try to find "a programmer's way" of thinking about filters and ultrafilters. [0] https://annals.math.princeton.edu/2019/189-2/p04 https://annals.math.princeton.edu/2019/189-2/p04
  - 082349872349872 4y ago
    > As a little challenge, try to find "a programmer's way" of thinking about filters and ultrafilters. As a programmer attempting to develop an intuition for filters, are the following at all close? - a filter is a funny kind of predicate (involving order shenanigans) - an ultrafilter is a classical predicate, with excluded middle.
    - ykonstant 4y ago
      Very good; your insight in your second observation in particular is excellent. But you can push the first observation much further. I will let other people think about it too before giving my own thoughts.
- kmill 4y ago
  I can't really compare non-standard analysis with filters due to not knowing much about NSA, but filters are a natural sort of completion of the poset of subsets, the pro-completion. Every subset can be naturally regarded as a filter (a principal filter), and I think of filters in general are sort of "thick" sets -- sets with some sort of infinitesimal fringe. There's also a helpful coincidence that open filters (filters on the poset of open subsets of a topological space) can be perfectly represented as filters. It makes sense to work with "functions" whose domains and ranges are filters. From this perspective, a function X -> Y is continuous at x if it can be restricted to be a function nbhd x -> nbhd f(x), where nbhd x denotes the principal open filter from all the open neighborhoods of x. If you're familiar with the germ at x of a smooth function f : X -> R, this is exactly the same concept as the restriction of f to a function nbhd x -> R. It's also possible to restrict to a germ at any given subset of f, which I think is neat. For example, you can restrict a smooth function to an infinitesimal neighborhood of a smooth submanifold. These are some of the reasons why I think that filters have some "user friendliness," once you get a feel for them.

defrost 4y ago

For those curious, the paper is about formal manipulation (computers!) in mathematical proof in the domain of geometric topology where a lot of hand waving (err, sorry, intuition) can go down. The result this is applied to is one by Smale (of the Horseshoe Map and other notions) that a sphere (ie abstract basketball 2D surface in 3 space) can be turned inside out without puncturing or creasing. Here's a 20 minute video that starts with an outline of the problem and then discusses approaches. https://www.youtube.com/watch?v=OI-To1eUtuU https://www.youtube.com/watch?v=OI-To1eUtuU This also may interest some: https://www.researchgate.net/publication/7942052_Visualizing_a_sphere_eversion https://www.researchgate.net/publication/7942052_Visualizing...

RBerenguel 4y ago
The co-author of the article linked has a very "fun" book on how to better draw on whiteboards, particularly for topology: https://link.springer.com/book/10.1007/978-0-387-68120-7 https://link.springer.com/book/10.1007/978-0-387-68120-7 His main example in the book is showcasing the sphere eversion.

kmill 4y ago

Here's the website where they kept track of the status of the Sphere Eversion Project: https://leanprover-community.github.io/sphere-eversion/ https://leanprover-community.github.io/sphere-eversion/ They have a dependency graph that shows the general structure of the argument: https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph_document.html https://leanprover-community.github.io/sphere-eversion/bluep...