Sofa problem may have been solved

Stream: maths

[Miyahara Kō]

https://arxiv.org/pdf/2411.19826
Peer review has not yet begun.
Who want to formalize this?

[Rida Hamadani]

I'm interested!
Also cc. @Jineon Baek

[Jihoon Hyun]

I'm also interested!
Since the author's in the channel, I'd wait for the author's response before making any decisions, though.

[Jineon Baek]

Regarding overall potential project plan:

• Thank you for your interest. I'd personally be thrilled to see the proof formalized.
• My main priority now is to have the proof reviewed by human experts, the most common way for academics as of now. As I will mostly be busy with this, I cannot commit too much time on formalization myself.
• The tools are elementary, but the proof is very long and will consume a lot of human-hours. I would encourage one to judge the opportunity cost of spending time on this vs. doing other things.
• On top of that, right now it is not the case that a formalization is _necessary_ like Kepler's conjecture. The proof, while long, should be readable by a human given sufficient time. Of course a full formalization will improve the credibility, but right now I have no good estimate of the additional gain from full formalization (would be happy to hear any thoughts on this).

Please do not misunderstand this as discouraging the formalization. I would love to see it formalized! It's just that I cannot lead the formalization effort as of now, and right now myself cannot guarantee what would be the benefit esp. given the potential work-hours needed.

[Jineon Baek]

Regarding technicalties:

• The full details of the proof begins with Chapter 2. I feel like they are written in a similar manner as a Lean blueprint - definitions and proofs strictly in logical order, with most details laid out. If enough people wants to formalize (after considerations above are made), I'd be happy to make a blueprint and explain the details at some point.
• We will need to work in both ends: the proof and the theoretical technicalties needed like this.
  • One will need basic vocabularies of so called 'Brunn-Minkowski theory'. That is, the collection of all convex bodies have algebraic structure (Minkowski sum and dilation), and that the surface area measure and area of a convex body K acts as a multilinear functional on K.
  • We also need Green's theorem and Jordan curve theorem - I am not sure if we have that in mathlib. On top of that we need a general version of Green's theorem for absolutely continuous functions - a.e. differentiable function.

[Miyahara Kō]

@Jineon Baek Thanks for the reply.
I myself cannot start a formalization project for this theorem because I have plans to find a better type system for Lean (which I felt was necessary in the process of proving the existence of definable non-Borel sets) and write it for my thesis.
However, I thought it would be very interesting if a prominent theorem could be formalized faster than it can be peer-reviewed, so I thought I would make a suggestion.
I welcome anyone who can start this formalization project.

[Esteban Martínez Vañó]

I'm also interested. I'm very new to Lean, but I'll be glad to work and learn from/with you in a project like this one :smiling_face:

I also think it would be very interesting to formalize it before the usual peer-review process finishes.

[Michael Rothgang]

I just looked at the preprint briefly: it mentions a bunch of theory that could be useful for other papers. Formalising that (and getting it into mathlib) seems like a useful contribution in any case. (And you'll certainly get help with that part!)

[Jineon Baek]

Michael Rothgang said:

I just looked at the preprint briefly: it mentions a bunch of theory that could be useful for other papers. Formalising that (and getting it into mathlib) seems like a useful contribution in any case. (And you'll certainly get help with that part!)

I agree.

• Abstract convex space might be a good place to start. Section 7.1. I said 'convex domain' there but its real name is cancellative convex space.
• Then the Brunn-Minkowski theory on convex bodies. Mixed volume, surface area measure, maybe good to have Minkowski inequality or Alexandrov-Fenchel though I do not use it in my work.

[Jineon Baek]

Esteban Martínez Vañó said:

I also think it would be very interesting to formalize it before the usual peer-review process finishes.

I personally think the way this can happen is when formalization people commit like 10x more hours a day, have full dedication compared to people who reads the paper. Formalization only happens when you completely assimilate all the details of the proof and do extra engineering, while to convince yourself that extreme level is not needed.

[Jineon Baek]

...but I'd be happy and humbled to be proved wrong!

[Miyahara Kō]

@Jihoon Hyun @Jineon Baek
This is unrelated to the topic, but yesterday in South Korea, the president declared martial law and the National Assembly was occupied by the military, threatening the country's democracy.
However, the lawmakers managed to get into the National Assembly and lifted martial law, thus averting a crisis.
I am glad that you are safe. I hope that the man will soon cease to be president.

[Jineon Baek]

We are doing good! Thanks and no worries

[Jihoon Hyun]

Jineon Baek 말함:

• The full details of the proof begins with Chapter 2. I feel like they are written in a similar manner as a Lean blueprint - definitions and proofs strictly in logical order, with most details laid out. If enough people wants to formalize (after considerations above are made), I'd be happy to make a blueprint and explain the details at some point.

Then maybe one group can start the formalization by defining the definitions in Chapter 2. May I, or will @Jineon Baek , or others, open a repository with a new lean project to work on?

[Jihoon Hyun]

By the way, we can use a template https://github.com/pitmonticone/LeanProject .

[Esteban Martínez Vañó]

Jineon Baek ha dicho:

Esteban Martínez Vañó said:

I also think it would be very interesting to formalize it before the usual peer-review process finishes.

I personally think the way this can happen is when formalization people commit like 10x more hours a day, have full dedication compared to people who reads the paper. Formalization only happens when you completely assimilate all the details of the proof and do extra engineering, while to convince yourself that extreme level is not needed.

Respect to the consensus of the mathematical community I think you are right, but for the peer-reviewing respect to to its publication in a good journal I'm not so sure being the paper so long :)

[Jineon Baek]

Esteban Martínez Vañó said:

Respect to the consensus of the mathematical community I think you are right, but for the peer-reviewing respect to to its publication in a good journal I'm not so sure being the paper so long :)

@Seewoo Lee convinced me along a similar line. I would like to do a quick consensus check. Please add the following emoji if you want to work on this. Think about it seriously before adding; see what I wrote at the top before starting.

:working_on_it: if you want to work on this project and speaks Lean moderately proficiently
(say, if you have an easy olympiad problem, then you can formalize it under couple hours; this is just a rough example and feel free to use your own judgement).

:construction: if you want to work on this project and you need to learn Lean while working on the it at the same time

[Yaël Dillies]

Regarding convex spaces, they are part of a huge upcoming refactor of mine to make convexity available in affine spaces. Here is my current prototype. Anyone wanting to work on them should feel free to contact me

[Jineon Baek]

Given the number of people serious of formalizing the sofa proof, right now I think it is best for us to keep the goal moderate and formalize the ground theory at our own pace. My suggestion is to start with building the theory of Brunn-Minkowski.
I will not lead the formalization effort, but feel free to ask me about the details of the math proof of sofa or the details of the list below.

• Define convex bodies on general Euclidean space R^d as closed, compact, and convex subset.
• Prove the fundamental theorem that K is a convex body if and only if it is the intersection of closed half-planes.
• Define the support function, mixed volume, surface area measure of a convex body K. Show multi-linearity of mixed volume etc.
• Show that the space of all convex bodies itself form an abstract convex space/cone with Minkowski sum and dilation.

[Junyan Xu]

• Define convex bodies on general Euclidean space R^d as closed, compact, and convex subset.

@Paul Reichert contributed mathlib3#16297 but is apparently working on category theory now in mathlib4 ...

[Junyan Xu]

• Prove the fundamental theorem that K is a convex body if and only if it is the intersection of closed half-planes.

This doesn't guarantee compactness, right? It should follow from geometric_hahn_banach_point_closed but I don't know if there is a more specialized result It's exactly iInter_halfSpaces_eq. Searching the hyperplane separation theorem produces many results about cones but not convex bodies.

[Mario Carneiro]

@Jineon Baek random typo report: the description of section 8.5 at the start of chapter 8 has an unfinished sentence

[Jineon Baek]

Junyan Xu said:

• Prove the fundamental theorem that K is a convex body if and only if it is the intersection of closed half-planes.

This doesn't guarantee compactness, right?

Apologies that I am being loose here. A precise statement would be: For a subset K of R^d, the followings are equivalent.

1. K is a convex body
2. K is bounded and can be written as an intersection of closed half-planes.
3. K is the intersection of its supporting half-planes in all angles.

I am also not sure if this exact statement is needed. Like you said, some hyperplane separation theorem with convex bodies is essentially what seems needed.

[Oliver Nash]

I think Brunn-Minkowski would make a nice self-contained project in its own right and I'd love to see it done as it is the key ingredient required to prove the isodiametric inequality and thus establish our Hausdorff measure normalisation by closing the sorry here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Hausdorff.20measure.20normalisation/near/466726879

[Paul Reichert]

Junyan Xu said:

• Define convex bodies on general Euclidean space R^d as closed, compact, and convex subset.

Paul Reichert contributed mathlib3#16297 but is apparently working on category theory now in mathlib4 ...

That's right -- right now I'm occupated with another project and don't want to commit to a second project. Sounds quite interesting though :-)

[Jineon Baek]

To those who showed interested in the formalization effort: I am now working with others to formalize the Brunn-Minkowski theory, which is necessary for the sofa thing to be formalized.

Check #maths > Brunn-Minkowski Inequality + Theory and let us know if you are interested there.