The 18 axioms for a complex Hilbert space consist of ax-hilex 8790, ax-hfvadd 8791, ax-hvcom 8792, ax-hvass 8793, ax-hv0cl 8794, ax-hvaddid 8795, ax-hfvmul 8796, ax-hvmulid 8797, ax-hvmulass 8798, ax-hvdistr1 8799, ax-hvdistr2 8800, ax-hvmul0 8801, ax-hfi 8867, ax-his1 8870, ax-his2 8871, ax-his3 8872, ax-his4 8873, and ax-hcompl 8992.

The axioms specify the properties of 5 primitive symbols, , , , , and .

If can prove in ZFC set theory that a class is a complex Hilbert space, i.e. that CHil, then these axioms can be proved as theorems axhilex (future), axhfvadd (future), axhvcom (future), axhvass (future), axhv0cl (future), axhvaddid (future) , axhfvmul (future), axhvmulid (future), axhvmulass (future), axhvdistr1 (future), axhvdistr2 (future) , axhvmul0 (future), axhfi (future), axhis1 (future), axhis2 (future), axhis3 (future), axhis4 (future), and axhcompl (future) respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex (future).