We essentially implemented this matrix version in Lean/mathlib to both compute the fibonacci number and generate an efficient proof for the calculation. https:

We essentially implemented this matrix version in Lean/mathlib to both compute the fibonacci number and generate an efficient proof for the calculation. https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/NormNum/NatFib.lean https://github.com/leanprover-community/mathlib4/blob/master... In practice this isn't very useful (the definition of Nat.fib unfolds quick enough and concrete large fibonacci numbers don't often appear in proofs) but still it shaves a bit of time off the calculation and the proof verification.