The closed graph theorem: a worked example with AI

The Baire category example included with Manifield is a set of working notes in functional analysis. It contains definitions, theorem statements, proofs and unfinished tasks, stored as plain Markdown files. You can browse the library and dependency graph without connecting an AI provider.

This walkthrough follows a specific gap in those notes: the final step of a draft proof of the closed graph theorem. The mathematical explanation below is written for this guide. The homepage's animated conversation illustrates the same step with a scripted exchange; an actual assistant conversation will vary with the model and your project.

#Open the notes and find the target

Follow the installation guide and open examples/baire-category/baire-notes from the public repository.

Search the library for Closed graph theorem, whose item id is thm-closed-graph. Its status is Proof drafted. You can also read the original item here.

The statement concerns Banach spaces $X$ and $Y$ and an everywhere-defined linear map $T:X\to Y$. It says that if the graph of $T$ is closed, then $T$ is bounded. The proof draft ends with a paragraph labelled Still to write.

#Follow the dependencies

The item lists the facts it uses:

• def-graph-of-an-operator defines the graph $G(T)$.
• lem-products-of-banach-spaces supplies the Banach product space.
• lem-closed-subspaces-are-banach makes the closed graph a Banach space in the restricted norm.
• cor-bounded-inverse supplies the bounded inverse theorem.

In the Dependency Graph, follow the bounded inverse theorem to the open mapping theorem and its prerequisites. This is how the local proof connects back to the Baire category argument elsewhere in the notes. The graph shows the dependencies recorded in the project; reading the statements and proofs is how you check that those links are justified.

#Locate the missing step

The product is equipped with the sum norm

$$\Vert (x,y)\Vert =\Vert x\Vert +\Vert y\Vert .$$

The draft has already shown that $G(T)$ is Banach. It defines the first-coordinate projection

$$P:G(T)\to X,P(x,Tx)=x.$$

Because $T$ is everywhere defined, $P$ is bijective. The sum norm makes $P$ bounded, and the bounded inverse theorem gives a bounded map $P^{-1}:X\to G(T)$.

The remaining task is to recover $T$ from that inverse and obtain a norm estimate. The important constraint is to do this using the product norm, while boundedness of $T$ is still the conclusion being proved.

#Ask for a focused proposal

If you connect AI, use Propose mode and ask:

Read thm-closed-graph, lem-products-of-banach-spaces and cor-bounded-inverse. Complete only the step marked “Still to write”. Justify the norm estimate from the product norm, preserve the statement and propose the edit for review. Keep the status at Proof drafted.

Prismo can read those items, discuss them and propose a change. Inspect the references and the proposed text before accepting it. The assistant guide explains the modes and their permissions.

#Check the argument yourself

Define the second-coordinate projection

$$Q:G(T)\to Y,Q(x,Tx)=Tx.$$

This map is linear, and the restricted sum norm gives

$$\Vert Q(x,Tx)\Vert =\Vert Tx\Vert \le \Vert x\Vert +\Vert Tx\Vert =\Vert (x,Tx)\Vert .$$

Thus $Q$ is bounded with operator norm at most one. Also $P^{-1}(x)=(x,Tx)$, so $T=Q{P}^{-1}$. Consequently,

$$\Vert Tx\Vert \le \Vert P^{-1}\Vert \Vert x\Vert .$$

That is the required bound. The estimate for $Q$ follows directly from the sum norm on the graph. In particular, it does not need an earlier estimate of $\Vert Tx\Vert$ in terms of $\Vert x\Vert$.

When reviewing a proposed edit, check all three points: the domain of $Q$ is the graph with its restricted norm, the proof justifies boundedness of $Q$, and the composition identity holds for every $x\in X$.

#Keep a draft separate from its review

Accepting a proposed paragraph changes the working notes. It does not by itself establish that every prerequisite and every step has been reviewed. Keep the status consistent with the evidence you have checked. An AI review can reach Review found no errors; human approval and formal verification are separate statuses controlled by you.

The example also includes conj-no-countable-hamel-basis, an exercise recorded as unresolved in these particular notes. Its conjecture status describes the notebook's progress. The result is classical and is not an open problem in the literature.

For your own project, the same workflow is useful: identify a precise gap, read its prerequisites, request a bounded change and retain the evidence for your review. Research mode extends this to separate lines of attack and independent checks, with explicit limits on model use.

#Try the workflow with your own notes

The app and this example are free and open source. Browsing the example needs no AI account. AI conversations and imports use your chosen provider or ChatGPT plan.

See studying advanced mathematics with AI for a reading workflow, sources and documents for working with books and papers, or the LaTeX graph tool to explore your file's explicit references in a browser.