Map Folding Enumeration Problem

### What is the conjecture

An $m \times n$ rectangular map has horizontal and vertical creases. Each crease is marked as a mountain fold (convex) or valley fold (concave). A **flat folding** is a valid configuration where the paper can be folded along all creases simultaneously such that the result lies in a plane without overlaps.

The map folding enumeration problem asks: **How many distinct flat foldings exist for a given m×n map with specified crease markings?**

For an $m \times n$ map where rows and columns can each be folded in mountain or valley configurations, a distinct folding corresponds to a valid 2D stacking order of the rectangles. The problem is equivalent to counting the number of permutations of the $m \times n$ cells (read left-to-right, top-to-bottom) that can be realized by a valid mountain-valley crease pattern.

**Known values** for square $n \times n$ maps:
- $1 \times 1$: 1 folding
- $2 \times 2$: 8 foldings
- $3 \times 3$: 1,368 foldings
- $4 \times 4$: 300,608 foldings
- $5 \times 5$: 186,086,600 foldings
- $6 \times 6$: 123,912,532,224 foldings
- $7 \times 7$: 129,950,723,279,272 foldings

No closed-form formula or efficient general algorithm is known.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://mathworld.wolfram.com/MapFolding.html, https://en.wikipedia.org/wiki/Map_folding, https://thatsmaths.com/2019/02/14/folding-maps-a-simple-but-unsolved-problem/, https://www.robertdickau.com/mapfolding.html, https://wikenigma.org.uk/content/mathematics/map_folding_problem

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-02-13)

Building blocks (1-3; from search results):
- Finite combinatorial structures and permutations (available in Mathlib)
- Graph-based representation of crease patterns
- Constraint satisfaction for flat-folding conditions

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of a "flat folding" configuration and validity constraints for 2D stacking orders
- Geometric or graph-theoretic characterization of which mountain-valley crease patterns admit flat foldings

Rating justification: The combinatorial counting framework (permutations, finite sets) exists in Mathlib, but formalizing the geometric constraints that determine which folding configurations are valid requires new definitions capturing the spatial/topological constraints of the folding problem. The core challenge is precisely defining what makes a folding "flat" in formal terms.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-52

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

The issue names no repository files, tests, or entry points. Begin by defining flat-folding configurations and their validity constraints in Lean, then establish a formal characterization before attempting the enumeration; done means the conjecture and its required definitions are formalized with supporting proofs.

Written by the indexing model from the issue text.