Vitushkin's Conjecture

Nobody has claimed this yet.

### What is the conjecture

A compact subset $K$ of the complex plane with finite 1-dimensional Hausdorff measure $H^1(K)$ is *removable for bounded analytic functions* if and only if it intersects every rectifiable curve in a set of zero arc length measure.

Equivalently, the analytic capacity $\gamma(K) = 0$ if and only if $K$ is purely unrectifiable in the appropriate sense (does not contain any rectifiable arcs in a quantifiable way).

The conjecture characterizes when a compact set is a removable singularity for bounded holomorphic functions in terms of geometric measure-theoretic properties related to projections and rectifiability.

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

**Sources:**
- https://en.wikipedia.org/wiki/Analytic_capacity, https://link.springer.com/book/10.1007/978-1-4419-6709-1, https://arxiv.org/abs/2204.05804

### Prerequisites needed

**Formalizability Rating:** 3/5 (0 is best) (as of 2026-03-08)

Building blocks (1-3; from search results):
- `Measure.hausdorffMeasure` and dimension theory (in Mathlib)
- Complex analysis foundations (`Complex`, analytic functions)
- Geometric measure theory concepts (arcs, rectifiability)

Missing pieces (exactly 2; unclear/absent from search results):
- Analytic capacity definition and its fundamental properties ($\gamma(K)$ for compact sets)
- Formalization of "removable for bounded analytic functions" and "purely unrectifiable" in the precise sense needed

Rating justification (1-2 sentences): Analytic capacity and the specific harmonic-analytic theory of removable sets are not in Mathlib, requiring significant new infrastructure around potential theory and boundary analysis. While basic measure-theoretic and complex-analytic foundations exist, the conjecture involves specialized concepts from harmonic analysis that would require substantial development.

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

* ams-30
* ams-42
* ams-28

### 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.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Start by checking the cited analytic-capacity sources and the repository's existing formal-conjecture structure. Confirm the precise definitions of analytic capacity, removability, and pure unrectifiability before attempting formalization; done means a mathematically accurate Lean statement with the required missing infrastructure identified or added.

Written by the indexing model from the issue text.