Automating Mathematical Reasoning: Interactions Between Proof Assistants, Computer Algebra Systems and Generative AI, at ICMS 2026

This is an OpenPGP/MIME signed message (RFC 4880 and 3156)
--===============8603613480135403634==
Content-Type: text/plain; charset="us-ascii"
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Disposition: inline

[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


--===============8603613480135403634==
Content-Language: en-GB, de-DE
Content-Type: multipart/signed; micalg=pgp-sha256;
 protocol="application/pgp-signature";
 boundary="------------LQOyi6w2L8YrpC4qrtB7mEez"

This is an OpenPGP/MIME signed message (RFC 4880 and 3156)
--------------LQOyi6w2L8YrpC4qrtB7mEez
Content-Type: multipart/mixed; boundary="------------LzDHXa99bj7mHngLVhs95ZGE";
 protected-headers="v1"
From: Mohammad Abdulaziz <[email protected]>
Reply-To: Mohammad Abdulaziz <mohammad.abdulaziz-3vygKqVCdQxaa/[email protected]>
To: [email protected], [email protected],
 types-announce-nHFbR+4dATOoZA3Q9b/[email protected], [email protected],
 [email protected], [email protected]
Message-ID: <0adb0dd6-d9ac-4166-8a2e-08752c7d3ee7-Re5JQEeQqe8AvxtiuMwx3w@public.gmane.org>
Subject: Automating Mathematical Reasoning: Interactions Between Proof
 Assistants, Computer Algebra Systems and Generative AI, at ICMS 2026
References: <31159ec0-6b55-4a09-b04c-d970ea09ad06-3vygKqVCdQxaa/[email protected]>
In-Reply-To: <31159ec0-6b55-4a09-b04c-d970ea09ad06-3vygKqVCdQxaa/[email protected]>
Autocrypt-Gossip: addr=mohammad.abdulaziz-3vygKqVCdQxaa/[email protected]; keydata=
 xsDNBGNxPTUBDADHiW5Xg6wPVFgFCJUfPs+FoTHC/cTyumEMkP9AGN1UAnCwcWFiOfD9U7/D
 zsrVz3tv5AsBqhI+pdB5+uX5SedfWLFLFae0gJDt4um4n4AqefkzqcOoKiHOjc/zFty8rSoe
 50MfhNUQxpjh9Bt5lkvZHhyneUp5RZt45aHaftWZaIttQj0SmQfUOlYm8sClhHDs45yvKUVF
 4AzQuGU8GTObbiHGDz4LLVF9f/EoGyqDFlYyztPrwqJS9aFL8K0O4TA+vTm1C39PqyKkseyI
 Y5EreB+dPTq1wrbLYFmIJNglmXyxmh1/UUP37vyc0d4BMmGjTHHF5e65mMHIw7tOXinV4MiO
 zqZkBJ/w1OniMsq1I+iRruA3dWw3XFOoq3ro+OYgk3ODPCDoNp4cyI4dKWCC/+xD+OH0kAdB
 qPyYnSnq7onZd073PtldsA49ZP5LxIrDW5XDw25LZmAbMEL0TuEuD2EWLkM5KY9e/VQxOSlg
 jYI4Qspc6Z0G1C5a24TQol0AEQEAAc0xTW9oYW1tYWQgQWJkdWxheml6IDxtb2hhbW1hZC5h
 YmR1bGF6aXpAa2NsLmFjLnVrPsLBBwQTAQgAMRYhBBi3EIhAELc7QLEp9JmUWNv0ZB/fBQJj
 cT02AhsDBAsJCAcFFQgJCgsFFgIDAQAACgkQmZRY2/RkH98RKAwAq51XFziFJ3i3Vu3X5bJJ
 QKKkIsRe++45BYoeFnLueXDimyXudv3Vekdlom3YS4n5rvzzf/TF3RRvRMJGLVRsZbOuBTbm
 F7+7C9qMXHNqH7ULBRIRarKQKkdJl9YESWJu9DslErZmyA9fE25XzbZNYDJ922r4dER2kMNF
 jVhCXYNYwHhF/agmcFBr1GGUcXeZq6LhltXApD/wdZPRUotSZsoMsk1EVFs+5uX8ViN+VqvT
 aeE2Xki6M62Rho/ObKHU5HSTEbgCsXpGgvuiOb5w72t1iceQ5X+GBYAd+Y2wgz5yuMaxj7UY
 uIS4I7fiOYCyKF/bH9G8K+Jx4NnUS6v/vQH1Pz4g5sevINreMKw182JbHZG5dMrnNhp0rcAi
 dgd4CNCukiT0fFPMcxCbbiv7SWDYh6DMYn1mq4VYtr/2YiKz1XOIJvMqNkYN8L5cs8wnh13F
 nmct8Qw2ioWyKXS7Q0RgeLWk/fZvycdRQQFB005C/Y0evChaL2afn439q7mOzsDNBGNxPTcB
 DADXxLIuNZYkavW9ZCXUJPZ2c41Pi+YEwSMo4g9tRf2rPQyhZNN0fE60QJJJgTiBxQkqpOPk
 MUuRGu82a5jPXyXVLklilb5gtfweSzJHVm1cjzV5MrWtvVb5w4VjmrM53gLpJGxAD0iW3H2r
 k/TTfgeXPS176bpkJfyh7iR+/DQlKqc7x8hdIB+WH236P/gr8ia6BHidLMd2SaCCY2cVnFdi
 hnJuqfwksZP6dWgrYqCPApiQjM8ibzz08Zs6p0K+BSzSJ9BSyNbpeXMAxRG+YInynzE+9WC3
 MvQympISDh8vCYoQf5SOgHi/jy7c99PLCb1ClxJPXVadmjX5mXycLN2G8z31O/7pa/jDfM7u
 G3YUTyyzrtu5yQgRmG7yTuV7HHnS/4xPOesrc9r0vLwgdS6maIiT8nupSRZZvFjTn3PzU51M
 4wxvILoXM5XU7HPyad19U/gVi8scy67S6Enbj9GQ0Aqe/X8cTEZgD0VI5cqoa9/9or6+znIV
 OZtUgrQnzRsAEQEAAcLA9gQYAQgAIBYhBBi3EIhAELc7QLEp9JmUWNv0ZB/fBQJjcT03AhsM
 AAoJEJmUWNv0ZB/fQh0L/R1Smeole8aEQaVZWsQ+8ZPKrITErqp1hW0VLqd5MUWt3/HDtETs
 bpr5G8L6uZYmACmlF9m75XgJfmtZJreieJqX5iF+qb+O2PbqAdldClbKeoXK6VSeUK+Ca4w0
 rSsUA2o0mEEK50RlAHme8hn/bIB0k+holTQ6rhfOVMKBp1eY2PC89Fj010QiKmEH4gwny69D
 GsoITExoH4dlpuYuLY/bMU3yXwUK8bYyZmFszBPQJyrk+tGQAVbJ0qCV1ZxREUaNuTDku+qv
 GIMBn8LfQus+iArtvC7xrnPY+AQNCCfDI+DG08YFo1k/xflSfpZUXVxd45b3K0GGNyKEcYwO
 oh4vdRWuqvDXIsjdo4RbDM4+OJrahz3pN61sjvjpAA+x86q2pwfP6pEm4zV0kuF+obHK6UDe
 Ynvk4I8ceEeoBwEd69uLtLtJGQkca3KytazPrpPoqrAUFcQkCVBUBVFfip8DU8OsqBW4tBGG
 wXv3hTzzdMGOzMqPbw8MvnBQtP1nhA==

--------------LzDHXa99bj7mHngLVhs95ZGE
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: base64

RGVhciBjb2xsZWFndWVzLA0KDQpXZSBpbnZpdGUgc3VibWlzc2lvbnMgb2Ygc2hvcnQgYWJz
dHJhY3RzIChhcHByb3hpbWF0ZWx5IDIwMCB3b3JkcykgZm9yIA0KY29udHJpYnV0ZWQgdGFs
a3MgaW4gdGhlIHNlc3Npb246IEF1dG9tYXRpbmcgTWF0aGVtYXRpY2FsIFJlYXNvbmluZzog
DQpJbnRlcmFjdGlvbnMgQmV0d2VlbiBQcm9vZiBBc3Npc3RhbnRzLCBDb21wdXRlciBBbGdl
YnJhIFN5c3RlbXMgKENBUykgDQphbmQgR2VuZXJhdGl2ZSBBSSB0byBiZSBoZWxkIGF0IHRo
ZSBJbnRlcm5hdGlvbmFsIENvbmdyZXNzIG9uIA0KTWF0aGVtYXRpY2FsIFNvZnR3YXJlIChJ
Q01TKSAyMDI2ICgyMOKAkzIzIEp1bHkgMjAyNiwgV2F0ZXJsb28sIENhbmFkYSkuDQoNClRo
aXMgc2Vzc2lvbiBmb2N1c2VzIG9uIHJlY2VudCBhZHZhbmNlcyBhdCB0aGUgaW50ZXJzZWN0
aW9uIG9mIHByb29mIA0KYXNzaXN0YW50cywgY29tcHV0ZXIgYWxnZWJyYSBzeXN0ZW1zIGFu
ZCBhbGdvcml0aG1zLCBhbmQgZ2VuZXJhdGl2ZSBBSSwgDQp3aXRoIHRoZSBhaW0gb2YgYWR2
YW5jaW5nIHRoZSBhdXRvbWF0aW9uIG9mIG1hdGhlbWF0aWNhbCByZWFzb25pbmcuIFdlIA0K
d2VsY29tZSBjb250cmlidXRpb25zIG9uIHRvcGljcyBpbmNsdWRpbmcgKGJ1dCBub3QgbGlt
aXRlZCB0byk6DQoNCiAgIC0gQWxnZWJyYWljIHNwZWNpZmljYXRpb24gYW5kIGZvcm1hbCBz
ZW1hbnRpY3Mgb2Ygc3ltYm9saWMgYWxnb3JpdGhtcw0KDQogICAtIEFJLWd1aWRlZCBhbmQg
Z2VuZXJhdGl2ZSBtZXRob2RzIGZvciBpbnRlcmFjdGl2ZSB0aGVvcmVtIHByb3ZpbmcNCg0K
ICAgLSBJbnRlZ3JhdGlvbiBvZiBwcm9vZiBhc3Npc3RhbnRzIHdpdGggQ0FTIGFuZCBzeW1i
b2xpYyBjb21wdXRhdGlvbiANCnN5c3RlbXMNCg0KICAgLSBGb3JtYWwgdmVyaWZpY2F0aW9u
IG9mIG1hdGhlbWF0aWNhbCBhbGdvcml0aG1zIGFuZCBjb21wdXRhdGlvbmFsIA0KbWV0aG9k
cw0KDQogICAtIExlYXJuaW5nLWJhc2VkIGFwcHJvYWNoZXMgdG8gbWF0aGVtYXRpY2FsIGRp
c2NvdmVyeSBhbmQgZm9ybWFsaXphdGlvbg0KDQpEZWFkbGluZSBmb3IgYWJzdHJhY3Qgc3Vi
bWlzc2lvbjogRmVicnVhcnkgMjMsIDIwMjYuDQoNCk1vcmUgaW5mb3JtYXRpb24gaXMgYXZh
aWxhYmxlIGF0Og0KaHR0cHM6Ly9pY21zLWNvbmZlcmVuY2Uub3JnLzIwMjYvc2Vzc2lvbjEu
aHRtbA0KDQpUbyBzdWJtaXQgYW4gYWJzdHJhY3Qgb3IgdG8gaW5xdWlyZSBmdXJ0aGVyLCBw
bGVhc2UgY29udGFjdCBhbnkgb2YgdGhlIA0Kc2Vzc2lvbiBvcmdhbml6ZXJzOg0KDQogICAt
IE1vaGFtbWFkIEFiZHVsYXppeiAoS2luZydzIENvbGxlZ2UgTG9uZG9uLCANCm1vaGFtbWFk
LmFiZHVsYXppekBrY2wuYWMudWspLA0KDQogICAtIFdlbmRhIExpIChVbml2ZXJzaXR5IG9m
IEVkaW5idXJnaCwgd2VuZGEubGlAZWQuYWMudWspLA0KDQogICAtIENyaXN0b3BoZXIgU2Fs
dmkgKEltcGVyaWFsIENvbGxlZ2UgTG9uZG9uLCBjLnNhbHZpQGltcGVyaWFsLmFjLnVrKSwN
Cg0KICAgLSBaaGVuZ2ZlbmcgWWFuZyAoRWFzdCBDaGluYSBOb3JtYWwgVW5pdmVyc2l0eSwg
emZ5YW5nQHNlaS5lY251LmVkdS5jbiksDQoNCiAgIC0gSnVqaWFuIFpoYW5nIChJbXBlcmlh
bCBDb2xsZWdlIExvbmRvbiwgemhpeXVhbi56aGFuZ0BpbXBlcmlhbC5hYy51ayksDQoNCiAg
IC0gTGlob25nIFpoaSAoQ2hpbmVzZSBBY2FkZW15IG9mIFNjaWVuY2VzLCBsemhpQG1tcmMu
aXNzLmFjLmNuKS4NCg0KV2UgbG9vayBmb3J3YXJkIHRvIHlvdXIgY29udHJpYnV0aW9ucy4N
Cg0KV2l0aCBiZXN0IHJlZ2FyZHMsDQpUaGUgT3JnYW5pemluZyBDb21taXR0ZWUNCg==

--------------LzDHXa99bj7mHngLVhs95ZGE--

--------------LQOyi6w2L8YrpC4qrtB7mEez
Content-Type: application/pgp-signature; name="OpenPGP_signature.asc"
Content-Description: OpenPGP digital signature
Content-Disposition: attachment; filename="OpenPGP_signature.asc"

-----BEGIN PGP SIGNATURE-----

wsD5BAABCAAjFiEE96O/NMZOikZKSd1ME5ifZTqZLY4FAmmQkVMFAwAAAAAACgkQE5ifZTqZLY5i
1Qv/T4yzgALVfSJhBqMW1q61fBPNuNbi3Lv/ojdOwD8k04J0Pu0eaId8/5vpVapnbNVFY0+twKXo
dS4UmQ30pZWrlDjHA8CM4XiMGIkLD4qw/g8h9fMzSrU8RhTgtOksU21w0LnU+rvNasrPSuDJbkXD
RA93MrrEmCLTa8GcOjE5DDqYRBCjqkNpgImUW7HCr+uHuUoE11B9vHcR22xjKS+QJqmmnpU9iMqn
RxxLdB0mPNvsfnkJV5L/dWRwbO80eTt/onhhxazYCcL/q2hX7Ld9conZ74auG58v0eOUjAnsa1BU
P6pFxKTQ874cA1UDqZvI9ThF6VdhS5V5S+eux43MSoGyO9PE8fqL9AVp+jHHfuQVW1u+TpLddcez
YXzgeknpd/5EjhT3UOL5ODbJgoW3Mrxc/B0XVo9Hik9eeuFrySzPkC6eYU8Kv6iU60E3mwVR8DFc
+rgkpn4UvX8OOQv8/pHmznkM3tllYojP4v0JuWJ1XyUck5PO35YhtYT0WhQm
=oKo1
-----END PGP SIGNATURE-----

--------------LQOyi6w2L8YrpC4qrtB7mEez--

--===============8603613480135403634==--