<div dir="ltr">Dear all,<br><div>I thought I'd join the stream of people sharing paper drafts, and point you toward the most recent version of a paper I plan to submit to ITP. While it is not directly connected to Matryoshka, I hope that some of you will find it interesting!</div><div><br></div><div><a href="http://www.andrew.cmu.edu/user/rlewis1/leanmm/leanmm_public_draft.pdf">http://www.andrew.cmu.edu/user/rlewis1/leanmm/leanmm_public_draft.pdf</a><br></div><div><br></div><div>The paper describes a user-extensible interface between the Lean theorem prover and Mathematica.</div><div><br></div><div>As always, comments are welcome before or after the deadline on Monday!</div><div><br></div><div>All the best,</div><div>-Rob</div></div>