Map Folding Realizability Problem (Edmonds, 1997)

### What is the conjecture

An $m \times n$ rectangular map has horizontal and vertical creases. Each crease is marked as either a mountain fold (convex) or a 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 or overlapping layers.

**The Map Folding Realizability Problem (Edmonds, 1997)**: Given an $m \times n$ rectangular map with specified mountain and valley fold markings on each crease, **what is the computational complexity of deciding whether a valid flat folding exists?**

In particular:
- Can this decision problem be solved in polynomial time?
- Is it NP-complete?
- Even the $2 \times n$ case (rectangles with only two rows) remains open.

This problem differs from the enumeration problem: rather than counting all valid foldings, we only need to determine whether *at least one* valid flat folding exists.

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

**Sources:**
- https://en.wikipedia.org/wiki/Map_folding, https://mathworld.wolfram.com/MapFolding.html, https://thatsmaths.com/2019/02/14/folding-maps-a-simple-but-unsolved-problem/, 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):
- Computational complexity theory framework (P vs NP) available in Mathlib via formal definitions of decision problems and Turing machines
- Finite rectangular grid structure and crease labeling (basic combinatorial objects)
- Encoding of mountain/valley fold specifications

Missing pieces (exactly 2; unclear/absent from search results):
- Formal characterization of what makes a folding "flat" and the geometric constraints that determine feasibility
- Reduction framework or hardness proof techniques for establishing NP-completeness of map folding

Rating justification: While P vs NP concepts exist in Mathlib, formalizing the map folding realizability problem requires careful definition of the geometric validity conditions for flat foldings. The main challenge is precisely specifying when a fold configuration is feasible in formal geometric terms, not the complexity-theoretic framework itself.

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

* ams-68
* 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)