Brown CS News

Robert Y. Lewis Co-Founds A New Formalized Mathematics Journal

    Click the links that follow for more news about Robert Y. Lewis and other recent accomplishments by our faculty.

    Brown CS faculty member Robert Y. Lewis has just co-founded the Annals of Formalized Mathematics, a new diamond open-access journal that will publish original articles about formalized mathematics and mathematical applications of proof assistants. Also known as interactive theorem provers, these tools are used to produce formally correct mathematics: users write definitions, theorems, and proofs in a specialized language and receive instant feedback from the computer about each line. Rob will serve as Managing Editor alongside Filippo A. E. Nuccio Mortarino Majno di Capriglio of the Université Jean Monnet Saint-Étienne in France.

    Rob and his co-founders see formalized mathematics as not just a mathematical discipline but an entirely new multidisciplinary field. “These tools,” they write, “have been used to develop large libraries of ‘known’ mathematics as well as to verify major recent or controversial results. Despite its young age, this discipline is blossoming at a very fast pace; it nowadays occupies a significant place in the mathematical horizon.”

    Typical papers will be written for an audience of mathematicians. They will not focus on the details of the tools themselves or on novel mathematical proofs but will describe the mathematical lessons learned during the formalization process. Submission guidelines for prospective authors are located here.

    For more information, click the link that follows to contact Brown CS Communications Manager Jesse C. Polhemus.