You can produce formulas fitting on more than one line using \[[ ... \]] or \{{ ... \}}.
The second form produces verbatim formulas similar to those produced by the pretty printer (with the same breaking scheme) like:
lesseq.rec2.N
= /\X
/\x,y:N
(X x -> /\z:N (x <= z -> z < y -> X z -> X (S z)) ->
x <= y -> X y)
: Theorem
The first form produces multi-line formulas using the same mathematical syntax
than \[ ... \] like:
examples.ex1.tex
However, breaking formulas in not an easy task. When you compile with LaTeX a file test.tex produced from an file using \[[ ... \]], a
file test.pout is produced. Then using the command pretty test (do
not forget to remove the extension in the file name), a file test.pin is
produced which tells LaTeX where to break lines. Then you can compile one
more time your LaTeX file. It may be necessary to do all this one more time
to be sure to reach a fix-point.
The formula produced in this way will use no more space than specified by the
LaTeX variable \textwidth. Therefore, you can change this variable if
you want formulas using a given width.