Time: 15:30
Speaker: Zack Dooley (Western)
Title: "An Introduction to Proof Assistants"
Room: MC 107

Abstract: Proof assistants are a variety of software tools which can be used to assist in proof writing and verifying mathematical statements. Recently, proof assistants have been gaining popularity not just for their ability to verify the correctness of complicated proofs, but also as a tool of collaboration for mathematicians. In this talk I will introduce the basics of what proof assistants are and how to use them, in particular, focusing on the proof assistant Coq. I will show how to write basic definitions and proofs in Coq and show how libraries can help us with collaboration and proof writing.

Time: 15:30
Speaker: Siyuan Deng (Western)
Title: "Symbolic-numeric algorithms for simplifying differential systems and their application to the determination of approximate Lie symmetry algebras"
Room: MC 327

Abstract: An important and challenging computational problem is to identify and include the missing compatibility (integrability) conditions for general systems of partial differential equations. The inclusion of such missing conditions is executed by the application of differential-elimination algorithms. Differential equations arising during modeling generally contain both exactly known coefficients and coefficients known approximately from data. Very little research has been done on this case. This talk focuses on our recent work on approximate differential-elimination methods. Those methods are applied to approximate Lie symmetry algebras defining systems of differential equations. We illustrate this with applications to a class of Schrodinger equations, and other systems. Methods for computing the reliability of the methods are given as well.