The notion of polyadic approximation originates in Girard's very first paper on linear logic, where it is proved that intuitionistic (and classical) theorems may be approximated arbitrarly well by purely linear theorems, i.e., theorems in what is technically called multiplicative additive linear logic (or the internal language of symmetric monoidal closed categories with finite products and coproducts). We will expore the consequences of taking this idea seriously, in particular extending it all the way up to cut-elimination/computation sequences (rather than just formulas/types or proofs/programs). The resulting theory, which is developed in the context of higher multicategories, is quite rich and has far reaching applications, inspiring in particular a type-theoretic proof of the Cook-Levin theorem (the result stating that SAT is NP-complete).