From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Authentication-Results: plum.tunbury.org; dkim=pass (1024-bit key; unprotected) header.d=inria.fr header.i=@inria.fr header.a=rsa-sha256 header.s=dc header.b=mQS/T4DG; dkim-atps=neutral Received-SPF: Pass (mailfrom) identity=mailfrom; client-ip=192.134.164.83; helo=mail2-relais-roc.national.inria.fr; envelope-from=caml-list-owner@inria.fr; receiver=tunbury.org Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by plum.tunbury.org (Postfix) with ESMTP id D56A9400A3 for ; Mon, 5 Jan 2026 14:24:34 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=inria.fr; s=dc; h=to:date:message-id:from:subject:reply-to:sender:list-id: list-help:list-subscribe:list-unsubscribe:list-post: list-owner:list-archive; bh=co4lE7Sp+AtWtovVnVzAyumVNvwR5mPtS1P6REfNMBE=; b=mQS/T4DG3AruaiauB8tipPaMgoxTRupXKLmB87MmMvnPcsgt9ptX/rMx oub3ztaUIZLn6Fp2v8fIyfB1Ro9n4DvrG2jNAOV32D+xYNhvy+TPqivy3 E8drf01aP1gr9OZ/csLn+PvwGCEiDi05ZNhupJpnK1HFSbXsYeFT8VwbO E=; X-CSE-ConnectionGUID: HIgVihVIRziFYfQS1TAhWQ== X-CSE-MsgGUID: X27CCaGLQNerHs4lZnsCbA== Authentication-Results: mail2-relais-roc.national.inria.fr; dkim=none (message not signed) header.i=none; spf=SoftFail smtp.mailfrom=caml-list-owner@inria.fr; spf=None smtp.helo=postmaster@prod-sympa-app.inria.fr Received-SPF: SoftFail (mail2-relais-roc.national.inria.fr: domain of caml-list-owner@inria.fr is inclined to not designate 128.93.162.27 as permitted sender) identity=mailfrom; client-ip=128.93.162.27; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="caml-list-owner@inria.fr"; x-conformance=spf_only; x-record-type="v=spf1"; x-record-text="v=spf1 include:mailout.safebrands.com a:basic-mail.safebrands.com a:basic-mail01.safebrands.com a:basic-mail02.safebrands.com ip4:128.93.142.0/24 ip4:192.134.164.0/24 ip4:128.93.162.160 ip4:128.93.162.3 ip4:128.93.162.88 ip4:89.107.174.7 mx ~all" Received-SPF: None (mail2-relais-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@prod-sympa-app.inria.fr) identity=helo; client-ip=128.93.162.27; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="postmaster@prod-sympa-app.inria.fr"; x-conformance=spf_only X-IronPort-AV: E=Sophos;i="6.21,203,1763420400"; d="scan'";a="257019419" Received: from prod-sympa-app.inria.fr ([128.93.162.27]) by mail2-relais-roc.national.inria.fr with ESMTP; 05 Jan 2026 15:24:34 +0100 Received: by prod-sympa-app.inria.fr (Postfix, from userid 990) id DB1D081A46; Mon, 5 Jan 2026 15:24:33 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by prod-sympa-app.inria.fr (Postfix) with ESMTP id 8913081A34 for ; Mon, 5 Jan 2026 15:23:03 +0100 (CET) X-CSE-ConnectionGUID: yKIvIZKATReaSetFQHzc2w== X-CSE-MsgGUID: MCTSEpq9Q+Cni+JN2LsB9w== IronPort-SDR: 695bc946_aSPg3zMi6FLdpQYiBDXPsn37ROYFHPE/+HCxUgnGG9oO1F8 +ITjINvUdW6gCouT+W5tmdLGfV0FhSU2NycvHLw== X-ThreatScanner-Verdict: Negative X-IPAS-Result: =?us-ascii?q?A0GhAwCcx1tp/wZZH8BaglmCGCmBB14xAwQLSYgnhSyLH?= =?us-ascii?q?5t3gX8GCQEDAQ1EDQQBAQMBA4R6BIxuHwcBBDAJDgECBAEBAQEDAgMBAQEBA?= =?us-ascii?q?QEBAQENAQEFAQEBAgEBAgQGAQKBChOGTw2CWztxgSUBAQEBAQEBAQEBAQEBH?= =?us-ascii?q?QIUHDtkL0gwAh4xE4MDgnMDEaJFkFuBAYMc2woJJIFSBoFNkQyCL0KCDYQOM?= =?us-ascii?q?YMfAQMYghODSIIvBIMwkWqIMYFmA1ksAVUTFwsHBYFmA4EGMjwyHYEjPhdzh?= =?us-ascii?q?F0faA4GgRGDUYI/hkYPiVqBBQMLbT03FBuVUBmDKYEQgV+mQaEOhCuhUwRJg?= =?us-ascii?q?3EBEo0TmVSZBqlBgWg9gUYMB3KDNU8DGQ+PVQECh1yCZrpAKDI8AgcLAQEDC?= =?us-ascii?q?ZIegUsBAQ?= IronPort-PHdr: A9a23:Yz0ovhynEz85lmrXCzLOwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z xCZva0m3QCUBM3y0LFttan/i+jYQ2sO4JKM4jgpUadncFsor/tTtCEbRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiTSybL9oM Bm6sQrdu80UjIZiN6o61wfErGZPd+lKymxkIk6ekQzh7cmq5p5j9CpQu/Ml98FeVKjxYro1Q 79FAjk4Km45/MLluwHMQgeW+HYSXXgYngJHDAbZ4h76WIzxsjbhuepmxCaaJ8z2QqsqVjmk8 qxmVQXniCYDNz4+7WHXlsl9h79VrR69uxByxZPfbYeIP/R8Y6zdZ8sXS3dfUMlfWSJPAYOyY pATA+YdIepUs5XxqkESoRa4GAKiBPnvyjhNhnLu0q01zeMhEQ/I3AE7A90Oq27YrND0NKgIV OC1zbPEwiveYPNL3zr29YfHfAw7r/6WQbJwbdTeyVMpFw7dklmdqZHoMjKU2+gQr2SX8fdtW +yshmI6qw98rCajy9kyh4TKiI8byl/K+CR3zosxK9O1S0F2bcK5HZdOtyyWK417Sd4sTWFvv SY10LwGuZijcSgP0psnwQLQa/yZfIiT/hLsSvyRLS1ii315Yr6/mhWy/VC6yuLiUMm7yldKr jFektbWsHACywLc6tCHSvt8+keuwzCP1xzT6uFeJkA0jaraJ4Qmwr4qmZoet1nIECzumEjuk aObclso9vKm5uj6eLnrpZuRO5V1hwz4L68ggNawAf4iPQgLR2Wb+fqz1Lnk/UDhWrpKlPg2k qjCsJDGO8sUvLO2DxVJ3Yk/8BazFTKm0NUCknkCLVJJYgyIgJX0O13WIfD4C+mwg0i0nTt2w /3KIKftD5vQInTZk7rseaxx5k9ExAo2199f5pZUCr8bIPL0X0/8rNPYAQE+Mwy6zebqE8ly1 pgEVWKKA6+WKqbSsV6S6u0xPuaMeZcZuCzhJPg9+/7ukXg5lEcBcqaz2JsXbGm0HvBnI0WCf XrhmcwBEGcPvgomVuPmklyCUThJZ3azRa0w/D87CJi+AYfFXY+imKaB0zujHp1KemBGDUiBH Wrwe4WLRfgMbyGcLNV5nzMKSLatU5Uh2g+wtAH50bRqNvDb+jcdtZLiz9h1+/Pcmgsv+jBuE 8udyHuBT2R1nmwSQj823bpzrlJgxVeeyaR3nv9YFd1W5/5RSgk0OpDTwfJmBd3uXAzNZsqGS FO8TdW8HT48Vso/zcYWbUhyA9milQjD3ySyDrEPi7GFGYE6/rrH33jpKcZy03bG27clj1khW sZBLXSoiLZw+VubO4mcx06QkqLvcaUHwAbM8n2CxCyAphcLfhR3VPDKUHcRaGPdtpL850rHT vmjBal0YUN61ceeJ/4SOZXShlJcSaK7UDy/S2e4mmPrQA2N2qvJd43yPWMUwCTaDkEA1QEV5 3ePcwYkVW+6u2yLKjtoGBr0Zl/0t/FkoSa0Q0g6wSmBdAtk1rOw+1gYieHPA+gL0Oc8sTw64 y5xAE772tvXD9SaoA80c6hbb90V60wB0GPQsg07M5C9fOh5nlBLVQNxsgv10glvTIVNlc9/t HQx0A97Mr6VyntIbTaZxoz9M7GRIWLpuhWuYqvXnFzSzb56448p7/I14xXmtQCtTQ859ml/l sJSyz2a74nLCwwbVdTwVFw2/l50veOSZC51/I7S2XB2VMv8+jbfx9IkAvckwRe8bp9eNq2DD gr7D8wdAYCnNuUrn1Gjah9MMvpV8eY4OMavdv3O36DOXq4okz+hg2pv65s710OF8is6R+LVn t4Ez/yewgqbRmLkll7y+svzmI1CeXQTBj/mmHKiX9cXNvw0I9Vuay/mOcC8y9RgioS4XndZ8 AXmHFYawIqyfgLUaVXh3ApW3EBRoHq9mCL+wSYn9lNh5qeZwiHKxPzvMRQdPWseDmZvilniC YOvydUbVU2pKQUliVH2gCSyj7gev6l5I2TJFA1Hci/4IUlpSe21t7OHYohC5I5i4m1HFe+7Z 16dULv0pRAXhjjiE2Vpzzc+bzi2u5/9knSWkUqlJW1o5DrccMB0nlLE4cDEAOVWxnwATTV5j j/eAh69OcOo9JOajcWLvue7XmOnHppdFEujhYyNsyW1zWZxRxi+lvWy3NDrDEA23DT62N9jS SjT5E+tOM+wjuLqYKQ5NkBzTEfx8c97Bp1znu5SzNkL1H4Wi4/UtXsLnGHvMMlKjKf3bX4DX zkOkJbe5Ano3lEmL2rcntOjEC7EhJswIYfpBwFekjgw5M1LFqqOublNnC8u50G9sRqUev9l2 DEU1fop7ncexeAPogskiCuHUdVwVQFVOzLhkxOQ4pWwtqJSMSygfL++2mJ1hpakDbiHo0dRV GuzKfJAVWdgq95yNl7Byii55Yzjdtf4ZslVsxydlhaGguRIYsF5hr8BgixpPnj4tHsuxrsgj BBg6pq9uZCON2Rn+K/qZ3wQfi2wfc4Y/SvhyLpPhsvDlZ76BY1vQ39YFIutV/+jFyge8OjqJ xrbWiNpsW+VQN+9VUee8Bs09iOVVcvycSHGYiFel4kqRQHBdhUF0UZNA2x8xcJ/T1nixcrqd Fp162Im/Ub27BRLze1sOl/0VWK6xk/gfD4wTNL3wAN+yAZE6g+VNMWf6rk2BCRE5ti6qxTLL GWHZgNOBGVPW0qeBlmlMKP8rd/Hu/OVAOazNZ6sKf2HtPBeWvGUxJmuzpou/jCCMd+KN2VjC Ptz01RKXHRwEcDU0zsVTClfmyXIZs+d7BCyn08/5ti46+juURnz6JGnAqFXMM5z9hm6x6yIL KiVhS98KHBV2o5NjX7Exb4D3UID3iFjcz7+dNZI/SXJTa/WhupWF0tCOnk1b5IOv/N6gFooW 4aTkN7+279mg+RgDl5EUQekgcS1fYkRJHn7MlrbBUGNPbDAJDvRwsixb7nvLN8YxOhSqRC0v i6WVkH5OTHW3TbkUB6hGepXyiSaNRlf/oyxb1w+bAqrBMKjcRC9PNJt2HcuxqYog3rRKWMGG TFmdkJWsrCZ4WVTie45Hm1I63sjIOWZ0XX8jaGQOtMdtv1lBT5xnuRR7SEhyrdb2ypDQeR8h CrYqtMGS7COm/OKyyF7XRNC7D1An8SOvExnOOPU+oQSAR4sEzoG9iOVCh0Ppp1oBsC94si4L /DEj+T2KT5H8pTZ8dZOX6Dp IronPort-Data: A9a23:wTTZtaMclg2aN2LvrR2Bk8FynXyQoLVcMsEvi/4bfWQNrUp3gWMPn 2EXDD3TMq7eZWr9edAkYdm1pkkEuMXSmNVkSHM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48D8hk/jOHuehYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWQtWo4ow/jb8k035ayv4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gvx4xc3B9q5pa3we0sMT6S6FVDmZq1+BsBOKjAbzsAD+v5T2Mg0MS+7uB3V9zxF8 +ihgLTrIesf0gIgr8xGO/VQO3kW0aSrY9YrK1Dn2SCY5xWun3cBX5yCpaz5VGEV0r8fPI1Ay RAXACEuTw6itcGf/Ii2Q9JhmuoaDNvgZpxK7xmMzRmBZRonaZnZRqTR+dJR0HE7jdsIGPfXY stfZDZyBPjCS0QeYBFMUdRuzaH27pX8W2UwRFa9qqcw7Wb7xxc31bnkNduTd9CXLSlQth/D+ zqXoT+oU3n2MvS64ga+32q119aMtiX6G6A0Tpmj3K911Qj7Kms7VERMCwflyRWjsWa1Utdbb kgV4TYGtrk37EXtT9/nXhT+rmTsg/IHc9NKFuwh9AyExuzf+ECcB2EBT3hMZMFOWNIKqSICx 3yogfLbJhVTirCccn+B2I60vzjoJn1ARYMdXhPoXTfp8vG6/99s0EuTE4s8eJNZmOEZDt0Z/ txrkMTdr+9P5SLz///nlW0rehr1znUJJyZsjuktYkqr7xlieKmubJGy5F7Q4J5oddnHEQTc5 SZbxJTDsYji6K1hcwTXEY0w8E2Bvp5pzRWD3QEyRfHNCRz2oBZPgry8EBkifR03bphslc7Bf UnSpw5L/55PLTOtY+dyYou0CqwXIVvITLzYuzG9RoQmX6Wdgyfco38yNBLJhjCw+KXu+IlmU aqmnQ+XJS5yIcxaIPCeHI/xCJd6l3xs9nCZXp3h0RWs3JyXYXPfG/9PM0KDYqp9pOmIqRncu YQXfcab6QRtYMunaAnu8KkXMQ8rK1o/DsvIsMB5TLOIDTdnP2ADMMXv540dVbZrpZkIqdeQz EqBAhdZ7HHdmUz4LR67byE/SbH3Ard6g3EJHQ0tGleK2XMyPJqm04kDfqBqeYsHye1H5tx3R skjZM+vLKluSDPG2jJFdrj7jtVoWyqKjDK0HRiOQWYAba87YjfW6/nmVAfL3wsfPBqd7McRj eWp6VLGfMAlWQ9nMvfzVNuu6FGA5V4mh+N4WhrzEOl5IUnD3tBjFH3ss6URPcoJFBTkwwma3 SawBTMzh7HEg60xwenzqZG0laWbOMogIRMCBEje16i8CgfC9Gn6wYNgbveBTQqAaEzKopedd cdn5NCiFsYYnWR6kZt2SJdq6qMc2+HBhZFnyiZcIXGaSGjzV51BJCGd0Nhtp5994OZTmTGLV 3Kl/vhYPrS0O/3ZLmMBGTp9bsm+0aA7pzqDy9U0P0Tw2wFv9pWlT0h5HkeBmQ5dHpRPIaInx uYQ4+sL4TO7ihAVMcu0sRoN1mWTL04vV7csmYEaDbTK1Csq6ABmSr7NBhDm5Kqgb413DXArB TuP3ozQqq95xHvdQ0EsFHPI4/VRta4OtD9O0lUGAVaDwfjBudMawzxT9m4RYjlO7xAazd92B HdnB3d1KYqK4T1sospJBEKoOgNZASym6l7D8EQImELZXnuXeDT0dkNlAtm0/Wcd7254VRpY9 uvByG/aDBDbTPuo1S42AUNYu/jvSOJqzTL7meelIt+kGqcraj+0k46sYms18yHcO/0Tv3Geh +dW/7dXU5bZZAowuKwwDreI2YsAEC6kIHNwetA/3acrM1yFRhSM92mvEX2hQuJMOP3AzmGgA eNMOM9kdkqzxQSOnB8hFI8OJL5FrNw17eokIoHUC20itp2dpSs0rJvv2DT3vzIvcfVTkOIWC IDYRxSdGEO+2FpWnG7sqpFfG2yaONMrWiz17NqXws4oSa0RgbpJSl4j9Lmes1G+EhpVzzjNs CztP6bpnvFfk6JylI7SI4B/LgSTK+Krct+X8Qq24u98XfmWPejg7woq+0TaZSJINr4sWvNyp 7SHkPjz+Gjn5L8WcWToq6OtJplzx/eZfbRoa5rsDXxggyG9dtfm4EID90CGOJV5qo5hyff9d TSoSvmbVIAzYMhc9k13eiIFMhc6CobLVInCix65jcyxDkk67VSaAvKhrHPnVDQOPGtAcZjzE RT9tPuS98hV5tYETgMNA/Z9RYR0Ohn/UK8hbMf8riScEnLuuF6Zp7/+jlA13Fkn0JVf/BrSu vophyQSdShefInB1tRYqJB/txFRB31mx+wxd0ccvdN6llhWyYLAwfs1af075lN8y0QeF60Uo BnGdy0nCCz4XHJJfQiUDBHLQFKEHuJXUjvmDmVBwq5XAhtawKuLG/1k9y5l4jF7diaLICRL7 z0B0iWYAyVdCa2FiQreCjJXTAunKj7nKqo0xH3A IronPort-HdrOrdr: A9a23:HXUcEaHxlWbW3krBpLqEgseALOsnbusQ8zAXPi9KJiC9Hvb4qy nRppomPHbP4V57ZJhKo7q90ce7LE80uaQY3bUs X-Talos-CUID: 9a23:azXR5G9gMn5EfGWIjpeVv183O94EQF708E3dKnS1FUhQaK+eE0DFrQ== X-Talos-MUID: 9a23:W0/33ARsI+RR3zlARXTJrw1ZGd9xsp3tI0YM0rcg4e2fH31vbmI= X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="6.21,203,1763420400"; d="scan'208";a="135096399" X-MGA-submission: =?us-ascii?q?MDE86fRlzz9trk/OBp26Zh6HwzlcYciS3WKw6x?= =?us-ascii?q?xK2zziK3tg2cEChLbEJgxTMTS8WbaOhpyZchi2RrD96uddx9jRPhRpyp?= =?us-ascii?q?ZYLR7brZ1srAcVgJrf4o4VrZQ4OeGnmtVX2kyxVeAST8Fmqe9HVgMI1F?= =?us-ascii?q?GlXuobJ31Y1g74hll0oJOarw=3D=3D?= Received: from armistead.cs.miami.edu (HELO armistead.ccs.miami.edu) ([192.31.89.6]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 05 Jan 2026 15:23:03 +0100 Received: by armistead.ccs.miami.edu (Postfix, from userid 3640) id 5BD01A0183A; Mon, 5 Jan 2026 09:22:48 -0500 (EST) To: User-Agent: mail (GNU Mailutils 3.14) Date: Mon, 5 Jan 2026 09:22:48 -0500 Message-Id: <20260105142248.5BD01A0183A@armistead.ccs.miami.edu> From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] Research positions in Theorem Proving in AI and Math Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 19422 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: , List-Subscribe: , List-Unsubscribe: , List-Post: List-Owner: List-Archive: Archived-At: The University of Manchester has several research positions in Theorem Proving in AI and Math available immediately: https://www.jobs.manchester.ac.uk/Job/JobDetail?JobId=34016 The positions are funded by the project "Learning to do Math with Vampires and Spiders", see https://www.renaissancephilanthropy.org/learning-to-do-math-with-vampires-and-spiders. For any questions please contact Prof. Andrei Voronkov at andrei@voronkov.com.