Update info.md with new intro text

site/info.md

@@ -8,7 +8,9 @@ layout: doc
 
 # Summary
 
-Ideas for the formalisation, Lean, [mathlib](https://leanprover-community.github.io/) workshop in Rome.
+Over the last several years computerized tools for verifying and manipulating proofs have become much more mature, and as a result formalized proofs have the potential to play a meaningful role in mathematical innovation and teaching well beyond their traditional role in the foundations of mathematics.
+
+This short program consists of three colloquium talks on major aspects of formalization, in terms of both underlying ideas and concrete implementations, together with a series of workshop-style sessions intended to give participants first-hand knowledge using the Lean language and associated tools.  We hope this will provide an introduction to the area for working mathematicians and advanced students in a variety of fields.
 
 - Duration: 3 days
 - Day 1: Intro to Lean; Day 2: Numbers, sets and functions; Day 3: Algebra, topology and analysis.