Why does NTRUEncrypt lack a formal security proof? Is there any particular reason why NTRUEncrypt lacks a formal security proof? That is, a demonstration that it achieves certain security notion (e.g. IND-CPA). I know there is a provable-secure variant from Stehlé and Steinfeld, but my question is regarding the original NTRU proposal.
NTRU, as it was originally introduced, is based on what people now call the "NTRU assumption", which really just assumes that it is difficult to break NTRU.  Annoyingly circular, but that's how it is.  Similar to how breaking RSA is not provably as hard as factoring (technically it is based on the "RSA assumption"), but people still think it is hard, NTRU was conjectured to be secure based on the fact that it is hard to find the shortest vector in a lattice (which is the private key).  The SVP problem is actually NP-complete.  However, you can't really make a secure cryptosystem based on an NP-complete problem.  You need some related problem with good average-case hardness to work with.  This was in 1996.

The paper you reference by Stehlé and Steinfeld does modify NTRU to be provably reducible to some standard lattice problems.  However, the problem they use (Ring Learning with Errors) was not formalized or studied until 2005.  So the answer really is that there was a lot of work on the complexity of lattice problems that still needed to be done when NTRU was published, and the authors didn't have the tools necessary to prove it secure at the time.