FP and math are the same concept.

The semantics of math are equation based.

Everything in the math universal language is defined as an expression or formula.

All proofs are based on this concept.

To translate this into programming think about what programming is? Programming rather being a single line formula is a series of procedures.

  1. add 1
  2. add 3
  3. repeat.

That is essentially what functional programming is. Fitting your entire program onto one line OR fitting it into a math expression.

The reason why you see multiple lines in FP languages is because of aliasing.

  m = b + c
  y = x + m

  y = x + (b + c) 

So functional programming, one line programs, formulas and equations in math, and immutability are essentially ALL the same concept.

That is why lean is functional. Because it's math.