I am currently teaching a seminar on mathematics and language, html. Rebecca Morris has successfully defended her thesis, Appropriate Steps: A Theory of Motivated Proof, and earned her PhD. I am contributing to the development of a new theorem prover, Lean. We have a tutorial, pdf, a system description, pdf, and a paper describing the elaboration algorithm, pdf. I taught a seminar on interactive theorem proving in the spring of 2015: course page. I gave a series of five lectures on proof theory and proof mining at the 2015 summer school in logic in Helsinki: html. I recently gave a series of four lectures on formal methods in mathematics at the Research Center for Computer-Assisted Research Mathematics and Applications (CARMA) at the University of Newcastle. You can find them under "Talks." The Open Logic Project is developing free open source logic textbooks. I have written a paper, "Mathematics and language": pdf. It is for a collection of essays, Mathematics, Substance and Surmise: Views on the Meaning and Ontology of Mathematics, edited by Ernest Davis and Philip Davis, to be published by Springer