Skip to content

Manifield A home for your theory.

A free, open-source macOS app for mathematical research with AI. Turn your notes into a library of definitions, lemmas and theorems, see what depends on what, and work with an assistant that reads your own definitions.

Download for macOS Source on GitHub

Free and open source. Version 0.1.3, for macOS 15 or later. Or open the example project first.

Start from what you already have.

Drop in your notes.
A .tex file or a PDF of what you have so far. Here: the example project's notes on Baire category and the big theorems of functional analysis.
The Organizer reads them.
Every definition, lemma, theorem and conjecture becomes its own item, and the proofs tell it what each one uses.
You review everything first.
Nothing is saved until you confirm. Check the links it found: on these notes, 14 had to be fixed by hand.

Baire category notes

Add files to the projectKeep PDFs as they are — read them in the app, and let agents search and read them on request. No model calls.

Import into the libraryBreak a LaTeX or PDF document into definitions, theorems and lemmas you review before anything is saved.

Drop a LaTeX (.tex) or PDF file here — or paste LaTeX below. Long documents are processed in parallel chunks; you can pause and resume at any time.

TEX

baire-working-notes.tex20.7 KB · LaTeX

Choose Another…Analyze with Organizer

Keep the original file in the projectReview before savingImport model: Default

Organizer is analyzing baire-working-notes.tex…

0 items proposed so far

You can switch to another tab — the import keeps running.

PauseCancel

Import time shortened

Review proposed items

27 of 27 selected — nothing is saved until you confirm.

CancelImport Selected

Complete metric spaces

def-complete-metric-spacesDefinitionProof drafted

§ baire-category

Nowhere dense, meagre, and residual

def-nowhere-dense-meagre-and-residualDefinitionProof drafted

§ baire-category · depends: def-complete-metric-spaces

Nested closed balls

lem-nested-closed-ballsLemmaProof drafted

§ baire-category · depends: def-complete-metric-spaces

Baire category theorem

thm-baire-category-theoremTheoremProof drafted

§ baire-category · depends: def-complete-metric-spaces, def-nowhere-dense-meagre-and-residual, lem-nested-closed-balls

Closed-cover form of Baire

cor-closed-cover-form-of-baireCorollaryProof drafted

§ baire-category · depends: thm-baire-category-theorem

Countable intersections of residual sets

cor-countable-intersections-of-residual-setsCorollaryProof drafted

§ baire-category · depends: def-nowhere-dense-meagre-and-residual, thm-baire-category-theorem

Complete spaces without isolated points

cor-complete-spaces-without-isolated-pointsCorollaryProof drafted

§ baire-category · depends: cor-closed-cover-form-of-baire

Normed and Banach spaces

def-normed-and-banach-spacesDefinitionProof drafted

§ banach-spaces-and-linear-operators · depends: def-complete-metric-spaces

Closed subspaces are Banach

lem-closed-subspaces-are-banachLemmaProof drafted

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces

Products of Banach spaces

lem-products-of-banach-spacesLemmaProof drafted

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces

Bounded linear operators

def-bounded-linear-operatorsDefinitionProof drafted

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces

Boundedness and continuity

lem-boundedness-and-continuityLemmaProof drafted

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces, def-bounded-linear-operators

Absolutely summable series

lem-absolutely-summable-seriesLemmaProof drafted

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces

Finite-dimensional subspaces are closed

thm-finite-dimensional-subspaces-are-closedTheoremCited literature

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces

Proper subspaces have empty interior

lem-proper-subspaces-have-empty-interiorLemmaProof drafted

§ banach-spaces-and-linear-operators · depends: def-normed-and-banach-spaces

Uniform boundedness principle

thm-uniform-boundednessTheoremProof drafted

§ uniform-boundedness-and-convergence · depends: def-bounded-linear-operators, lem-boundedness-and-continuity, cor-closed-cover-form-of-baire

Pointwise limits of operators

cor-pointwise-limits-of-operatorsCorollaryProof drafted

§ uniform-boundedness-and-convergence · depends: thm-uniform-boundedness, def-bounded-linear-operators

Convergence from a dense subspace

thm-convergence-from-dense-subspaceTheoremCited literature

§ uniform-boundedness-and-convergence · depends: def-bounded-linear-operators, def-normed-and-banach-spaces, cor-pointwise-limits-of-operators

Generic unboundedness

cor-generic-unboundednessCorollaryProof drafted

§ uniform-boundedness-and-convergence · depends: thm-uniform-boundedness, thm-baire-category-theorem, def-nowhere-dense-meagre-and-residual

Approximate openness

lem-approximate-opennessLemmaProof drafted

§ open-mapping-and-its-consequences · depends: cor-closed-cover-form-of-baire, def-normed-and-banach-spaces, def-bounded-linear-operators

Geometric-series lifting

lem-geometric-series-liftingLemmaProof drafted

§ open-mapping-and-its-consequences · depends: lem-absolutely-summable-series, lem-boundedness-and-continuity

Open mapping theorem

thm-open-mappingTheoremProof drafted

§ open-mapping-and-its-consequences · depends: lem-approximate-openness, lem-geometric-series-lifting

Bounded inverse theorem

cor-bounded-inverseCorollaryProof drafted

§ open-mapping-and-its-consequences · depends: thm-open-mapping, lem-boundedness-and-continuity

Equivalence of comparable complete norms

cor-equivalence-of-comparable-complete-normsCorollaryCited literature

§ open-mapping-and-its-consequences · depends: cor-bounded-inverse

Graph of an operator

def-graph-of-an-operatorDefinitionProof drafted

§ closed-graphs · depends: def-normed-and-banach-spaces, lem-products-of-banach-spaces

Closed graph theorem

thm-closed-graphTheoremProof drafted

§ closed-graphs · depends: def-graph-of-an-operator, lem-products-of-banach-spaces, lem-closed-subspaces-are-banach, cor-bounded-inverse

No countable Hamel basis

conj-no-countable-hamel-basisConjectureConjecture

§ a-question-about-dimension · depends: thm-finite-dimensional-subspaces-are-closed, lem-proper-subspaces-have-empty-interior, cor-closed-cover-form-of-baire

Complete metric spaces

def-complete-metric-spaces · Definition · Proof drafted · § Baire category

Statement

For a metric space $(X, d)$ , write $B (x, r) = {y \in X : d (x, y) < r}, B (x, r) = {y \in X : d (x, y) \leq r} .$ The second notation denotes the closed ball; it need not be the closure of the open ball. A sequence $(x_{n})$ is Cauchy if, for every $ε > 0$ , there is $N$ such that $d (x_{m}, x_{n}) < ε$ for $m, n \geq N$ . The space is complete if every Cauchy sequence converges in $X$ . A set is dense if it meets every nonempty open subset of $X$ .

Simulated interface. The items, ids and links are the example project's; the import time is shortened. Splitting notes into items uses an AI model.

Pick a theorem. See what it needed.

Every result knows what it rests on. Click one in the graph and its whole argument lights up, all the way down to the definitions.

Closed graph theorem rests on 16 earlier results. Its longest chain of dependencies is 7 steps long.

Choose a result to explore

Baire category notesExplore

TypeStatusAll sections

Definitions & axiomsMain resultsSupporting resultsOpen questions

Unfinished proof

Simulated interface. The 27 items and 48 links of the example project. Colours are the app's item families.

A library you'd want to read.

Your results, typeset, grouped by section and searchable. Open one and you see its statement, its proof and what it depends on, with your own notation rendered the way you wrote it.

Baire category notesExploreNew Item

Baire category theorem

thm-baire-category-theoremTheoremBaire category

3

Baire category theorem

thm-baire-category-theorem · Theorem · Proof drafted · § Baire category · depends on: def-complete-metric-spaces, def-nowhere-dense-meagre-and-residual, lem-nested-closed-balls

Statement

Every complete metric space is a Baire space (Definition (def:category)). Equivalently, if $U_{1}, U_{2}, \dots$ are open dense subsets of a complete metric space $X$ , then $⋂_{n = 1}^{\infty} U_{n}$ is dense in $X$ .

Proof

The assertion is immediate if $X$ is empty. Otherwise, let $V$ be any nonempty open set. Choose $x_{1}$ and $0 < r_{1} \leq 2^{- 1}$ so that $B (x_{1}, r_{1}) \subseteq V \cap U_{1}$ . This is possible because $V \cap U_{1}$ is nonempty and open: choose an open ball inside it, then use a strictly smaller radius for the closed ball. Inductively choose $B (x_{n + 1}, r_{n + 1}) \subseteq B (x_{n}, r_{n}) \cap U_{n + 1}, 0 < r_{n + 1} \leq 2^{- (n + 1)} .$ Lemma (lem:nested-balls) gives a point in all these closed balls. It belongs to $V$ and every $U_{n}$ . Since $V$ was arbitrary, the intersection is dense.

Simulated interface. The example project's items and statuses, rendered by the app's own code. Try the search, or By Type in the sidebar.

Your notation stays yours.

Each project keeps a notation file, which every agent reads, and a file of LaTeX macros. Macros in a.tex file you import are picked up automatically. Write \norm{x} in your notes and the library shows it typeset, and the assistant writes it the same way.

\norm{Tx}\le\norm{P^{-1}}\,\norm{x}

∥ T x ∥ \leq ∥ P^{- 1} ∥ ∥ x ∥

Baire category notes

NotationMath MacrosOne definition per line, e.g. \newcommand{\A}{\mathcal{A}} — applied to all math rendering in the app.Save

\newcommand{\N}{\mathbb{N}}\newcommand{\R}{\mathbb{R}}\newcommand{\C}{\mathbb{C}}\newcommand{\K}{\mathbb{K}}\newcommand{\norm}[1]{\lVert #1\rVert}\newcommand{\interior}{\operatorname{int}}\newcommand{\Span}{\operatorname{span}}\renewcommand{\qedsymbol}{}

One folder of plain files.

Your whole theory is a folder on your Mac. Every result is a Markdown file with a few lines of metadata on top; your notation, your macros and your research memory are files next to them.

Open it in any editor. Keep it in git. Sync it however you like. Point Claude Code or Codex at it and they read and write the same files Manifield shows you. If you've used Obsidian, it's the same idea: your notes are files you own, and the app is a good way to read them.

theory

Choose a file

---
id: thm-closed-graph
type: theorem
name: Closed graph theorem
status: proof-drafted
depends_on: [def-graph-of-an-operator, lem-products-of-banach-spaces, lem-closed-subspaces-are-banach, cor-bounded-inverse]
resolves: []
tags: [operator, closed-graph, boundedness, banach-space]
source: baire-working-notes.tex
section: closed-graphs
order: 4001
---
## Statement
Let $X$ and $Y$ be Banach spaces and let $T:X\to Y$ be an everywhere-defined linear map. If its graph is closed in the sense of Definition~\ref{def:graph}, then $T$ is bounded.

## Proof
By Lemma~\ref{lem:product}, $X\times Y$ is Banach. The graph $G(T)$ is a closed linear subspace, so Lemma~\ref{lem:closed-subspace} makes it Banach in the restricted sum norm. The projection $P:G(T)\to X$, $P(x,Tx)=x$, is linear, bijective, and bounded because $\norm{x}\le\norm{x}+\norm{Tx}$. Corollary~\ref{cor:bounded-inverse} gives a bounded inverse $P^{-1}:X\to G(T)$.

**Still to write:** introduce the second-coordinate projection $Q:G(T)\to Y$, prove its norm estimate, and use $T=QP^{-1}$ to obtain an explicit bound for $\norm{Tx}$ in terms of $\norm{x}$. The boundedness of $Q$ must come from the product norm, not from assuming the conclusion that $T$ is already bounded.

thm-closed-graph.md

Markdown document · 1 KB

Baire category notes

Closed graph theorem

thm-closed-graphTheoremClosed graphs

4

Closed graph theorem

thm-closed-graph · Theorem · Proof drafted · § Closed graphs · depends on: def-graph-of-an-operator, lem-products-of-banach-spaces, lem-closed-subspaces-are-banach, cor-bounded-inverse

Statement

Let $X$ and $Y$ be Banach spaces and let $T : X \to Y$ be an everywhere-defined linear map. If its graph is closed in the sense of Definition (def:graph), then $T$ is bounded.

Proof

By Lemma (lem:product), $X \times Y$ is Banach. The graph $G (T)$ is a closed linear subspace, so Lemma (lem:closed-subspace) makes it Banach in the restricted sum norm. The projection $P : G (T) \to X$ , $P (x, T x) = x$ , is linear, bijective, and bounded because $∥ x ∥ \leq ∥ x ∥ + ∥ T x ∥$ . Corollary (cor:bounded-inverse) gives a bounded inverse $P^{- 1} : X \to G (T)$ .

Still to write: introduce the second-coordinate projection $Q : G (T) \to Y$ , prove its norm estimate, and use $T = Q P^{- 1}$ to obtain an explicit bound for $∥ T x ∥$ in terms of $∥ x ∥$ . The boundedness of $Q$ must come from the product norm, not from assuming the conclusion that $T$ is already bounded.

Simulated Finder and Manifield windows on the example project's real folder. Choose a file in Finder and Manifield shows the same item. Browse the folder on GitHub, or read how it is laid out.

Your references, not half-remembered ones.

Import the books and papers you actually use. Each becomes a source the assistant can search and cite, result by result, instead of "I think there was a paper about this".

A citation points at the book's own statement, written source:item-id, so you can open it and check. Results you cite without proof get their own status, Cited literature, and show up in your graph. The full text of a book is read only when you allow it.How sources work

Baire category notes

SourcesThe Elements of Euclid, Book IShow GraphActions

All types

Source overview

original.tex

I.47

casey-euclid:prop-i-47 · Proposition · Cited literature

Statement

In a right-angled triangle (ABC) the square on the hypotenuse (AB) is equal to the sum of the squares on the other two sides $(A C, B C)$ .

Simulated interface, searching the real text of John Casey's translation of Euclid (1885, public domain).

An assistant that has read your work.

Ask about your theorems by name. The assistant reads them before it answers, so it works from your actual definitions rather than a vague memory of the subject.

Every result it mentions is a link: open it beside the conversation and keep reading. It can draft new results or changes to existing ones, and by default each comes to you as a proposal you accept or reject. It can also run small computations to test a conjecture on examples, and it keeps the code next to the result. What the assistant can do

Baire category notes

Complete only the step marked “Still to write” in thm-closed-graph, and propose the edit for review.

→ read_theory_item thm-closed-graph

→ read_theory_item cor-bounded-inverse

→ read_theory_item lem-products-of-banach-spaces

The draft already has a bounded inverse $P^{- 1} : X \to G (T)$ from cor-bounded-inverse. For the missing step, let $Q : G (T) \to Y$ , $Q (x, T x) = T x$ . It is linear, and

∥ Q (x, T x)∥ = ∥ T x ∥ \leq ∥ x ∥ + ∥ T x ∥ = ∥(x, T x)∥,

so $∥ Q ∥ \leq 1$ , from the sum norm of lem-products-of-banach-spaces and not from assuming $T$ is bounded. Since $T = Q P^{- 1}$ , we get $∥ T x ∥ \leq ∥ P^{- 1} ∥ ∥ x ∥$ for every $x$ .

→ propose_theory_edit thm-closed-graph

I've proposed this as an edit to thm-closed-graph for you to review. Its status stays Proof drafted until the proof is reviewed.

Ask Prismo about your theory… (⏎ send · ⇧⏎ new line)Propose

Simulated interface. A scripted conversation about the example project's unfinished closed graph proof; the item ids, statements and the missing step are real. When the proposal arrives the app opens it for review; Done returns to the conversation, where any blue id opens beside it.

Know which parts are solid.

Every result has a status, so you can see at a glance which parts of the theory are solid and which are still hopes.

The assistant can take a result as far as Review found no errors. The last steps are yours alone: only you can mark a result as approved, as cited literature or as formally verified. Manifield has no proof assistant built in yet, so Formally verified is a status you set by hand.

ConjectureA statement you believe
TestedChecked on examples, with the code kept
Proof draftedA written proof exists
Review found no errorsAn independent review found no gap
Human approvedYou checked it yourselfOnly you
Formally verifiedChecked by a proof assistantOnly you

Suppose you have checked these results yourself. Now you find a gap in Approximate openness: open its status menu in the window and set it back to Proof drafted.

Baire category notes

Approximate openness

lem-approximate-opennessLemmaOpen mapping and its consequences

3

Approximate openness

lem-approximate-openness · Lemma · Proof drafted · § Open mapping and its consequences · depends on: cor-closed-cover-form-of-baire, def-normed-and-banach-spaces, def-bounded-linear-operators

Statement

Let $X$ be normed, let $Y$ be Banach, and let $T \in L (X, Y)$ be surjective. There is $δ > 0$ such that $B_{Y} (0, δ) \subseteq T (B_{X} (0, 1)) .$ The overline here means closure in $Y$ , not the image of a closed ball.

Proof

Surjectivity implies $Y = ⋃_{n \geq 1} T (B_{X} (0, n))$ and hence $Y = ⋃_{n \geq 1} T (B_{X} (0, n))$ . Corollary (cor:closed-cover) gives $N \geq 1$ , $y_{0} \in Y$ , and $r > 0$ with $B_{Y} (y_{0}, r) \subseteq T (B_{X} (0, N))$ . For $∥ y ∥ < r$ , both $y_{0} + y$ and $y_{0}$ belong to this closure. Choose $a_{k}, b_{k} \in B_{X} (0, N)$ with $T a_{k} \to y_{0} + y$ and $T b_{k} \to y_{0}$ . Then $T (a_{k} - b_{k}) \to y$ and $∥ a_{k} - b_{k} ∥ < 2 N$ , so $B_{Y} (0, r) \subseteq T (B_{X} (0, 2 N))$ . Scaling by $1/ (2 N)$ gives the assertion with $δ = r / (2 N)$ . The notation for balls and bounded operators is from Definitions (def:banach) and (def:operator).

Simulated interface. The dependencies are the example project's; the alert is the app's own wording.

Experimental: research mode.

You give it a problem. First it writes the problem down as a precise statement and freezes it, so the conventions are clear and it can't quietly change what it is trying to prove.

Then a director chooses directions (look for a counterexample, try this method, first establish that property) and hands each one to a separate agent that works only on that approach. A claimed solution counts only after independent checks.

It is experimental and it can use a lot of tokens. Most labs build tools like this as closed systems; it would be good to have one that mathematicians can read, change and shape.How research mode works

k-Domination Theory

ProgramsLimitsContinue

Boundedness of Open 2-Domination Ratioactive

3 assignments431K tokens of 6M4m so farupdated 3 Aug 2026

Not running3 Aug 2026

The program is not running. Continue to resume, or send guidance to resume with it.

Guidance for the director…

Sending resumes the program with your message.

Assignments

3

2 finished

Findings

1

latest 3 Aug 2026

Solution claims

0

none yet

Challenges

0

none yet

Tokens

431K

7% of 6M

Assignments 3View all

Friendship graph exact construction

Completed the explicit-family draft and internal review.

Finished · Planned · 151K tokens

Universal-vertex transfer audit

Created lem-matching-universal-vertex-specialization (proof-drafted), deriving for

G_{t} = K_{1} \lor (t K_{2})

:

γ (G_{t}) = 1

,

γ_{2} (G_{t}) = t + 1

, and

δ (G_{t}) = 2

for all

t \geq 1

.

Finished · Planned · 262K tokens

Attempt the boundedness mechanism

Queued · Planned · 18K tokens

Recent activityOpen log

4 items added to the library, 2 of them at Review found no errors.

23:33

Universal-vertex transfer audit finished: 2/2 tasks completed.

23:33

Finding published (reduction): Proof-drafted universal-vertex reduction.

23:31

Friendship graph exact construction finished: 2/2 tasks completed.

23:31

SpendLimits

431,373 of 6,000,000 tokens

Friendship graph exact construction: 151K Universal-vertex transfer audit: 262K Attempt the boundedness mechanism: 18K

Friendship graph exact construction

Finished · Planned · cheap · 151K tokens

Friendship graph exact construction: Lead with the friendship graphs $F_{t} = K_{1} \lor t K_{2}$ .

Kill-criterion audit for $F_{t} = K_{1} \lor t K_{2}$ : derive the exact two-case constraints for every $t \geq 1$
Draft and review the explicit-family counterexample: $δ (F_{t}) = 2$ , $γ (F_{t}) = 1$ , and $γ_{2} (F_{t}) = t + 1$ — depends: 1 — review

Universal-vertex transfer audit

Finished · Planned · standard · 262K tokens

Universal-vertex transfer audit: Audit and generalize the mechanism through a universal-vertex transfer formula: for $G = K_{1} \lor H$ , distinguish whether the new hub belongs to a $2$ -dominating set.

Audit the universal-vertex transfer equivalence, including the omitted-hub condition — review
Specialize the audited transfer formula to $G_{t} = K_{1} \lor (t K_{2})$ and issue the exact unbounded-ratio counterexample — depends: 1 — review

Attempt the boundedness mechanism

Queued · Planned · expensive · 18K tokens

Attempt the boundedness mechanism: Take the opposite prior seriously: attempt to convert a minimum dominating set into a $2$ -dominating set under $δ (G) \geq 2$ , using private-guard structure from lem-min-degree-two and the classical bound rather than accepting the pilots.

Test the universal-hub family symbolically: derive exact $γ (G_{t})$ and $γ_{2} (G_{t})$ for $G_{t} = K_{1} \lor C_{3 t}$ , and validate the formula by reproducible exhaustive subset enumeration for an explicitly stated finite range of $t$ — review
Conditional on task 1 not firing the kill criterion, formulate and test the sharpest private-guard exchange lemma converting a minimum dominating set to a $2$ -dominating set under $δ (G) \geq 2$ ; explicitly isolate whether universal hubs are excluded by a necessary hypothesis — depends: 1 — review
Conditional on tasks 1–2 leaving the boundedness thesis viable, draft a complete absolute-bound theorem with an explicit constant $C$ , citing def-k-domination, lem-min-degree-two only at its actual proof-drafted status, and thm-cockayne-bound; prove every new exchange step or report the precise obstruction — depends: 2 — review

Simulated interface showing a real run from the sample project (3 August 2026): its goal, contract, branches, finding, library changes and token counts. It was made with an earlier version of research mode and is laid out here as today's dashboard shows a program. Its result, that friendship graphs make γ₂/γ unbounded, is known; the run rechecked it. Click Goal, or the tabs.

Try it.

No account and no server. Your project is a folder on your Mac. If you use AI, requests go straight to the provider you choose, with your own API key or your ChatGPT account.

Download Manifield
Version 0.1.3, for macOS 15 or later, Apple silicon or Intel. Open the disk image and drag Manifield to Applications.
Open the example
The Baire notes from this page are in the repository. Open the baire-notes folder in Manifield; browsing it needs no AI and no account.
See your own LaTeX as a graph
Drop a .tex file into this website and see the graph its \ref links make. Nothing is uploaded.
Walk through Euclid
Book I of the Elements as a graph. Pythagoras rests on 40 earlier results.

Working from your notes: studying advanced mathematics with AI and a worked example of the closed graph theorem.

Setting up AI, the Python sandbox and models per task: install and connect AI.

Made by one person, early.

I built Manifield for my own research and made it open source in October 2026. It is early, it is written by one person, and there are rough edges. I would like to hear what you think: where it breaks on your notes, and what would make it worth using for your work.

Open an issue or start a conversation on GitHub. The code is GPLv3, and contributions are welcome.

Stanisław