nForum

I don’t know what’s up, but the page “Join of Simplicial Sets” seems to have been blanked by an anonymous user.

https://ncatlab.org/nlab/show/join+of+simplicial+sets

Now on PhysicsForums-Insights: A first Idea of Quantum Field Theory.

The chapters will be appearing incrementally. The first one is at

Mathematical Quantum Feld Theory 1 – Geometry

In a strict sense, that’s right.

However, in a more relaxed sense, which is more typical of how mathematicians really work, it’s hard to see this as much of a problem. (I don’t claim you’re saying it is a big problem, just explaining our perspective.) Firstly, to what are you comparing a Globular proof - a handwritten proof? Clearly, neither are strictly formal, and the Globular proof has the advantage of being fully explicit. No proof (because proving it by hand is too complicated)? Then Globular wins by default. A HoTT proof in Coq? OK, then maybe HoTT wins, but as we’ve discussed before, there are not that many proofs well-suited to formalization in both Globular and Coq. (Consider the Perko knot isotopy proof, compared to a proof in Coq that uses any sort of non-algebraic structure like a universal property.)

Also, note that handcrafted proofs are often carried out in an informal semistrict style anyway! For example, see a lot of the work of Scott Carter and collaborators on knotted surfaces calculations, which are taking place in a braided monoidal bicategory; they don’t stop to worry too much about the definition of semistrict 4-category, they just let geometry guide them. The same is true for a lot of the Morse-theoretic calculations of people like Chris Douglas, Andre Henriques and Chris Schommer-Pries; for example, Andre Henriques has an explicit sphere eversion proof which takes place formally in a semistrict 6-category.

Also, I would expect that if an expert in some “trusted” definition of 4-category looks at the singularity structure that Globular is using, they would say, “yeah, those rules are in my definition of 4-category, implicitly or explicitly”. And I think often this would be such an easy process, a Globular proof would give them a very good sense of how to construct a proof using their definition. (Of course, it would be nice to talk to some experts (like you Mike!) and see if they agree.) Perhaps more likely would be that they have some proof already in their definition of 4-category, and not see how to write it as a Globular proof. So they might say “hey, your definition of semistrict 4-category is not general enough.” And maybe they would be right (although I don’t think so), time will tell.

Note that even if we had proved that every weak 4-category is equivalent to a semistrict 4-category by our definition, that would only take you half way to fully trusting the Globular formalization: you would also need to prove that the source code of Globular implements the definition correctly. This is far from straightforward; as you know, writing a proof assistant is far more complicated than just “typing in the definition of the logical system”. And Globular is written in Javascript, which does not lend itself to formal verification, to say the least.

(By the way, using Javascript made Globular quite easy (in a relative sense) to write and debug; I don’t think Globular would exist today if we’d tried to write it in a more traditional programming language for computational logic. And if we’d succeeded, you’d have to download some crummy installer to use it, rather than just click on a link in your browser; and it would only exist on some platforms; and nobody would use it. So for many good reasons, being very formal is quite low down our list of priorities at the moment.)