Introduction

• Role of proofs in teaching engineering mathematics:
  • show why a statement is true → promoting understanding
  • provide "warrants" i.e. convincing arguments
  • basic mathematical competency in SEFI curriculum
    • to understand the notion of proof and to recognise the central ideas in proofs
• Common problems of students:
  • understanding the general logic of a proof
  • coping with ∀ or ∃ statements
  • realizing, what exactly remains to be proven at a certain step
• Proof assistants:
  • programs to construct proofs in simple steps
    • provide immediate feedback of the current proof status
    • give hints how to progress further
    • insert simple logical steps or computations automatically
  • popular examples: Coq, Isabelle, Lean
  • used in teaching mathematics and computer science
• Assessing their usefulness for engineering mathematics:
  • formalize basic examples
    • complex numbers
    • calculus
    • linear algebra
  • applying Lean 4
    • extensive documentation
    • huge mathematical library
    • very supportive community