diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 58a476bdc..9f7c9cf1b 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -123,6 +123,7 @@
         - [The solver](./solve/the-solver.md)
         - [Canonicalization](./solve/canonicalization.md)
         - [Coinduction](./solve/coinduction.md)
+        - [Proof trees](./solve/proof-trees.md)
 - [Type checking](./type-checking.md)
     - [Method Lookup](./method-lookup.md)
     - [Variance](./variance.md)
diff --git a/src/solve/proof-trees.md b/src/solve/proof-trees.md
new file mode 100644
index 000000000..e0904d946
--- /dev/null
+++ b/src/solve/proof-trees.md
@@ -0,0 +1,50 @@
+# Proof trees
+
+The trait solver can optionally emit a "proof tree", a tree representation of what
+happened while trying to prove a goal.
+
+The used datastructures for which are currently stored in
+[`rustc_middle::traits::solve::inspect`].
+
+## What are they used for
+
+There are 3 intended uses for proof trees. These uses are not yet implemented as
+the representation of proof trees itself is currently still unstable.
+
+They should be used by type system diagnostics to get information about
+why a goal failed or remained ambiguous. They should be used by rustdoc to get the
+auto-trait implementations for user-defined types, and they should be usable to
+vastly improve the debugging experience of the trait solver.
+
+For debugging you can use `-Zdump-solver-proof-tree` which dumps the proof tree
+for all goals proven by the trait solver in the current session.
+
+## Requirements and design constraints for proof trees
+
+The trait solver uses [Canonicalization] and uses completely separate `InferCtxt` for
+each nested goal. Both diagnostics and auto-traits in rustdoc need to correctly
+handle "looking into nested goals". Given a goal like `Vec<Vec<?x>>: Debug`, we
+canonicalize to `exists<T0> Vec<Vec<T0>>: Debug`, instantiate that goal as
+`Vec<Vec<?0>>: Debug`, get a nested goal `Vec<?0>: Debug`, canonicalize this to get
+`exists<T0> Vec<T0>: Debug`, instantiate this as `Vec<?0>: Debug` which then results
+in a nested `?0: Debug` goal which is ambiguous.
+
+We need to be able to figure out that `?x` corresponds to `?0` in the nested queries.
+
+The debug output should also accurately represent the state at each point in the solver.
+This means that even though a goal like `fn(?0): FnOnce(i32)` infers `?0` to `i32`, the
+proof tree should still store `fn(<some infer var>): FnOnce(i32)` instead of
+`fn(i32): FnOnce(i32)` until we actually infer `?0` to `i32`.
+
+## The current implementation and how to extract information from proof trees.
+
+Proof trees will be quite involved as they should accurately represent everything the
+trait solver does, which includes fixpoint iterations and performance optimizations.
+
+We intend to provide a lossy user interface for all usecases.
+
+TODO: implement this user interface and explain how it can be used here.
+
+
+[`rustc_middle::traits::solve::inspect`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/traits/solve/inspect/index.html
+[Canonicalization]: ./canonicalization.md
\ No newline at end of file