We'll talk about modern
proof assistants: what they are, and
their common features and differences. Also about decision procedures, and
how they can be added to a proof assistant without extending its "trusted
core". Are proof assistants the next evolutionary step in representing
mathematical results (just like LaTeX) ?