<html xmlns:v="urn:schemas-microsoft-com:vml" xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<!--[if !mso]><style>v\:* {behavior:url(#default#VML);}
o\:* {behavior:url(#default#VML);}
w\:* {behavior:url(#default#VML);}
.shape {behavior:url(#default#VML);}
</style><![endif]--><style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Aptos;}
@font-face
{font-family:"Trebuchet MS";
panose-1:2 11 6 3 2 2 2 2 2 4;}
/* Style Definitions */
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:#467886;
text-decoration:underline;}
p.xmsonormal, li.xmsonormal, div.xmsonormal
{mso-style-name:x_msonormal;
margin:0in;
font-size:11.0pt;
font-family:"Aptos",sans-serif;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;
mso-ligatures:none;}
@page WordSection1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.WordSection1
{page:WordSection1;}
--></style><!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1027" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]-->
</head>
<body lang="EN-US" link="#467886" vlink="purple" style="word-wrap:break-word">
<div class="WordSection1">
<div>
<div>
<p class="xmsonormal"><span lang="EN-GB"> Dear all, <o:p></o:p></span></p>
<p class="xmsonormal"><span lang="EN-GB"> <o:p></o:p></span></p>
<p class="xmsonormal"><span lang="EN-GB">Our seminar speaker for Monday is Dr. Tyler Josephson, Assistant Professor of Chemical, Biochemical, and Environmental Engineering at the University of Maryland, Baltimore County. The title of his talk is "Writing Provably-Correct
Software using Lean". I met him this summer during a conference and learned that he is using a software language to write and check mathematical derivations, which I found to be quite exciting. Below are the details of his seminar:<o:p></o:p></span></p>
<p class="xmsonormal"><span lang="EN-GB"> <o:p></o:p></span></p>
<p class="xmsonormal"><b>Writing Provably-Correct Software using Lean</b><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"> <span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal">When developing new methods for molecular simulation, eliminating bugs can be challenging. Programming languages like Python, FORTRAN, and Julia flag syntax errors, but don't (and cannot) catch errors in math or program logic - these must
be rooted out by human experts. These issues can be managed by following best practices in software development (such as writing tests alongside the program), but even these do not guarantee that code is correct. Probabilistic programs like Monte Carlo are
especially notorious.<span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal">Lean is a new programming language whose type system enables it to describe and check the logic of advanced math proofs. By translating derivations in science and engineering into math proofs in Lean, we get a computer-checked proof that
the derivations are mathematically and logically correct. We’ve translated the derivations of Langmuir and BET adsorption theory, as well as proofs about ideal gas thermodynamics and the kinematic equations of motion [1]. We can also write software for scientific
computing in Lean, and write proofs <i>about</i> the functions in our execution pipeline, providing guarantees that they have certain properties. Our prototype program performs BET surface area analysis using functions that are logically connected to a formal
derivation of BET adsorption theory. In the future, we aim to build LeanMD and LeanMC, formally-verified molecular dynamics and Monte Carlo software logically linked to formal derivations in classical and statistical mechanics.
<span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal">[1] Bobbin, M., Sharlin, S., Feyzishendi, P., Dang, A. H., Wraback, C. M., Josephson, T. R., ``Formalizing chemical physics using the Lean theorem prover."
<i>Digital Discovery</i>, (2024)<span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"><a href="https://nam11.safelinks.protection.outlook.com/?url=https%3A%2F%2Fdoi.org%2F10.1039%2FD3DD00077J&data=05%7C02%7Ceecs_mscs%40listserv.ohio.edu%7C07a55689f9064815512808dcdda4ab50%7Cf3308007477c4a70888934611817c55a%7C0%7C0%7C638628946549110593%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=%2B63AxCt75Uf90tIiykFm1d1zgP87ZKR2jquCiRirs74%3D&reserved=0" originalsrc="https://doi.org/10.1039/D3DD00077J" shash="mIdhb9qzs5ryVrYosHMmvySbP6Gmf42AHdkPReUDrgdvpnz/Y6w71ULG4XiqejIlltlfr8Oeb8wnWSG5Bk4QYC0ur0Tzqbw6k73/rPiBCLabNsYjIDrLhldHLcDzNkzp+XDVO7PBjKt9hKfw4fSHe3hgTB9NaXPNrJFOG9UVzS0=">https://doi.org/10.1039/D3DD00077J</a><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"> <span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal">This work is primarily supported by the NSF CAREER Award #2236769<span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"> <span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"> <span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"> <span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"><!--[if gte vml 1]><v:shapetype id="_x0000_t75" coordsize="21600,21600" o:spt="75" o:preferrelative="t" path="m@4@5l@4@11@9@11@9@5xe" filled="f" stroked="f">
<v:stroke joinstyle="miter" />
<v:formulas>
<v:f eqn="if lineDrawn pixelLineWidth 0" />
<v:f eqn="sum @0 1 0" />
<v:f eqn="sum 0 0 @1" />
<v:f eqn="prod @2 1 2" />
<v:f eqn="prod @3 21600 pixelWidth" />
<v:f eqn="prod @3 21600 pixelHeight" />
<v:f eqn="sum @0 0 1" />
<v:f eqn="prod @6 1 2" />
<v:f eqn="prod @7 21600 pixelWidth" />
<v:f eqn="sum @8 21600 0" />
<v:f eqn="prod @7 21600 pixelHeight" />
<v:f eqn="sum @10 21600 0" />
</v:formulas>
<v:path o:extrusionok="f" gradientshapeok="t" o:connecttype="rect" />
<o:lock v:ext="edit" aspectratio="t" />
</v:shapetype><v:shape id="Picture_x0020_2" o:spid="_x0000_s1026" type="#_x0000_t75" alt="A person wearing glasses and a suit
Description automatically generated" style='position:absolute;margin-left:0;margin-top:0;width:186pt;height:227.25pt;z-index:251658240;visibility:visible;mso-wrap-style:square;mso-width-percent:0;mso-height-percent:0;mso-wrap-distance-left:9pt;mso-wrap-distance-top:0;mso-wrap-distance-right:9pt;mso-wrap-distance-bottom:0;mso-position-horizontal:left;mso-position-horizontal-relative:text;mso-position-vertical:absolute;mso-position-vertical-relative:line;mso-width-percent:0;mso-height-percent:0;mso-width-relative:page;mso-height-relative:page' o:allowoverlap="f">
<v:imagedata src="cid:image001.jpg@01DB0F49.2B715B00" o:title="A person wearing glasses and a suit
Description automatically generated" />
<w:wrap type="square" anchory="line"/>
</v:shape><![endif]--><![if !vml]><img width="248" height="303" style="width:2.5833in;height:3.1562in" src="cid:image001.jpg@01DB0F49.2B715B00" align="left" hspace="12" alt="A person wearing glasses and a suit
Description automatically generated" v:shapes="Picture_x0020_2"><![endif]>Dr.
Tyler R. Josephson is an Assistant Professor in Chemical, Biochemical, and Environmental Engineering at the University of Maryland, Baltimore County. He received his B.S. in Chemical Engineering from the University of Minnesota in 2011 and his Ph.D. in Chemical
Engineering from the University of Delaware in 2017, after which he was a postdoctoral associate in the University of Minnesota Chemistry Department until 2020. In 2018, he spent time as a visiting scientist in the Mathematics of AI department at IBM Research.
At UMBC, he leads the AI & Theory-Oriented Molecular Science (ATOMS) Lab, developing computational methods for molecular simulation and automated discovery of scientific theories. Techniques used in the ATOMS Lab include quantum chemistry, Monte Carlo, symbolic
regression, and formal theorem proving using Lean. Dr. Josephson received the NSF Graduate Research Fellowship and is the 35th Laird Fellow at the University of Delaware. His research is supported by the National Science Foundation and the Department of Energy,
including the NSF CAREER Award for “Automated Reasoning to Advance Chemical Theory.”
<span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"><span lang="EN-GB"> <o:p></o:p></span></p>
<p class="xmsonormal"><span lang="EN-GB"> <o:p></o:p></span></p>
<div>
<p class="xmsonormal" style="background:white"><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">Sumit Sharma</span><span style="font-size:10.5pt;color:#62594E;border:none windowtext 1.0pt;padding:0in"><br>
</span><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">Associate Professor</span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal" style="background:white"><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">Department of Chemical and Biomolecular Engineering</span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal" style="background:white"><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">181 Stocker Center</span><span style="font-size:10.5pt;color:#62594E;border:none windowtext 1.0pt;padding:0in"><br>
</span><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">1 Ohio University</span><span style="font-size:10.5pt;color:#62594E;border:none windowtext 1.0pt;padding:0in"><br>
</span><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">Athens OH 45701-2979</span><span style="font-size:10.5pt;color:#62594E;border:none windowtext 1.0pt;padding:0in"><br>
</span><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in">T: 740.593.1425</span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"><span style="font-size:10.5pt;color:#666666;border:none windowtext 1.0pt;padding:0in;background:white">M: 503.209.7165</span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"><span style="font-size:10.5pt;color:black;border:none windowtext 1.0pt;padding:0in;background:white"><a href="mailto:sharmas@ohio.edu"><span style="color:blue">sharmas@ohio.edu</span></a></span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal"><span style="font-size:10.5pt;color:black">website: <a href="https://nam11.safelinks.protection.outlook.com/?url=http%3A%2F%2Fsharma-research.com%2F&data=05%7C02%7Ceecs_mscs%40listserv.ohio.edu%7C07a55689f9064815512808dcdda4ab50%7Cf3308007477c4a70888934611817c55a%7C0%7C0%7C638628946549110593%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C0%7C%7C%7C&sdata=9Q2a4pShy5P7wH9Ts5%2BCLmTo76Na0SP12%2B3d3ZH%2F1Yg%3D&reserved=0" originalsrc="http://sharma-research.com/" shash="dj5b6S7+uujUuDnwNZLQ3CJGPYM5to8/JvC4Z3CqCac+brJQi/ETuYPWqqo+Z4aMx1byN7fDTgGjvIDPkPFOVaO+HdLTHtGf82ISP3Mb8RzoisxzzGQl5hUgVeXEhA1ayEo0BUvNJMhNmivUFcVskQ0SAQ1d+SjKCGUTzy4ls9g=">
<span style="color:blue">http://sharma-research.com/</span></a> </span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal" style="line-height:18.0pt;background:white"><span style="font-family:"Trebuchet MS",sans-serif;color:#62594E"><img border="0" width="237" height="67" style="width:2.4687in;height:.6979in" id="x_Picture_x0020_2" src="cid:image006.gif@01DB0F48.99040100"></span><span lang="EN-GB"><o:p></o:p></span></p>
<p class="xmsonormal" style="background:white"><b><span style="font-size:10.5pt;color:#006633;border:none windowtext 1.0pt;padding:0in">Russ College of Engineering and Technology</span></b><span lang="EN-GB"><o:p></o:p></span></p>
</div>
<p class="xmsonormal"><span lang="EN-GB"> <o:p></o:p></span></p>
</div>
</div>
</div>
</body>
</html>