Skip to Content.
Sympa Menu

coq-club - [Coq-Club] AITP 2025 FINAL CALL FOR CONTRIBUTIONS - EXTENDED DEADLINE May 12

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] AITP 2025 FINAL CALL FOR CONTRIBUTIONS - EXTENDED DEADLINE May 12


Chronological Thread 
  • From: Josef Urban <josef.urban AT gmail.com>
  • To: Josef Urban <Josef.Urban AT gmail.com>
  • Subject: [Coq-Club] AITP 2025 FINAL CALL FOR CONTRIBUTIONS - EXTENDED DEADLINE May 12
  • Date: Mon, 5 May 2025 23:59:18 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=josef.urban AT gmail.com; spf=Pass smtp.mailfrom=josef.urban AT gmail.com; spf=None smtp.helo=postmaster AT mail-pl1-f179.google.com
  • Ironport-data: A9a23:O3QTh6M+o96D9b7vrR0Mk8FynXyQoLVcMsEvi/4bfWQNrUom0zIAn 2seWT3QaKrZYGb0fYwlPNmy9hsPu57Qy4I3T3M5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYQLNNwJcaDpOtvre8E435pwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGX9KivM/e1/NHsWPKs/1bp1DHl/9 cEHfWVlghCr34pawZq+Q+how9wndYzlZdxO/H5nyj7dALAtRpWrr6fiv4cJmmdtwJoXQbCHO JtxhTlHNHwsZzVNPUwaBtQjhu2hgFHwdjRZrBSeoq9fD237lVUsgOm1bIGNEjCMbf50mwXFp TjixmP0M08lBISxyDmC+23504cjmgugBdtKS+zmnhJwu3WYwXVWAxkLX3OgsPyhgwi/XcheI goa4EITQbMa8UWqSpzlW0T9rifb71gTXN1fF+B84waIokbJ3+qHLlNdHh5/cM0eju83YxsFi l2Eh+LpOCM65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8N5bYvXnHoYLLUKlsuAZDw0c1 NxjkcTTr7AajMpOz6HiuF6e3GPqqZ/OQQo4oA7QWwpJDz+Vhqb0PuRECnCCsp6sybp1qHHf5 RDofODAtogz4WmlznDlfQn0NOjBCwy5GDPdm0VzOJIq6i6g/XWuFagJv20gfxcybpZVJ2C5C KM2he+3zM8MVJdNRf8nC79d9+xwnMAM6Py8BqmNMYMUOvCdiifcrH0wPBf4M5/RfLgEyvxmY cjKL65A/F4VDqNoyDf+RuEWl9cWKtMWlAvuqWTA503/i9K2PSbLIZ9caQfmRr5jsMus/l6Om /4BbJTi9vmqeLevCsUh2dVLdQhSRZX6bLiqw/Fqmhmre1I4RDF9W6eJmNvMueVNxsxoqwsBx VnlMmcw9bY1rSevxdyiMyg4NOHcTtxkoGglPCchG1+t1jJxKcys9aoTPd9/N7Uu6OUpn7Y+Q ugnavewJK1Fag3G3DABMrj7johpLyqwiSy0YiGKXTkYfrxbfTLvxOPKRAXU2RcrMjuWruo7+ r2p6RPaS8EMRiNkF8fnV8isxFKQ41kYweJ7YFTUKfZMaGHTwZhMOS/svKVmPfNWORHnwx2E3 T23GjYdn/HG+KUuwenKhIeFjoanKPR/FUxkBFvm7a66GC3Z32i7y6pSebysUQGGcVjr6YOeZ elx5NPtAs0txVplndJ1LOd28PgY+dDqmY5/8i1lO3f6N3KQFbJqJyi97/ll76Fi6OdQhlqrZ xip5NJfBLSuPfHlGn43IC4OTLyK9dMQqwnowcUFGmfIzw4pw+PfSmRXBQeGtwJFJrgsMI8F/ /YoiPRL1yOB0CgVIvS0pQEK0V+TL04wcbQt7bAbJ47JtjAF6H9/Zb7kNyunx63XNvttNBExL y62lZjyoe1W5nD/fkoZEVnP2utghqoyhi1a8W9aJ3m0novqu/xm+jxQ7jU9cSpNxDplze9YG zZmJm91F4q07hZqg8lxBTmsEj5eGSzDq1DQykQIpkLdXUKHRmzAF0xjGOevrWQy0XNQQShfx 56ckF3aaDfNeNrg+Bc9Qmt3gqXHYeEp0zbdieeLOt+gHagqRRbE2YiQPXEprTnjCuMP3Hz3n /FgprtMWPeqJBwurL0eIKjE8KYbVzSvBnFIGNNl94M3RVDsQim4g2WyGhrga/F2BqL49GGjA JZTPeNJbRO10RiOoh09BaIhJ7xVnuYj1OEde4HEdHI3jL+CkgVH6J7g1DDypGsOceVclcwQL oDwdTXbNkeygXBSuXHGregaG26eTOQHWjbB37GOwL1UL64AjeBiSlFt872Wu37ODhBr0SjJt yz+ZojX7ddY96JSo6XWHJ9+WjqEceHIaLzQ8SSYkch/UtfUAMKf6yIXsgbGOipVD5swWvN2t 7KHj/Dv1miYvrxsC2H9sLuCHplv+s+dcrd2MMX2DX8ChgqEepbmzCUi8lCCC65isY1i9Oj+Y CCneu6cSMUzZ+5N4FF0Nw1PDAc7CYnsS6Xr+BOGsPWHDyYC3Tz9LN+I8WHjaUdZfHQqP6LSJ xDVufG8wMJxt6VJWQE5As95D69CIFPMXbUsc/vzv2K6CkiqmlazhavwpyE/6D3kCmi2L+ii2 MjrHiPBTRWVvL3E6Pp7sIYo5x0eMytbsNkKJ0kY/4Z7tiC+AGs4Nt8iCJQhCKxPsynMxZr9N SDsbmwjNH3HZg56Uy7AufbtYgTOIdY1GIbJFmR8tQfcISK7H5iJD7Zd5z9tqSU+MCfqyOa8b 8oS4DvsNxy22YtkXvsX+uf9u+p82/fG3TgdzCgRSSAp78o2Wt3mFUCNHTahkQTCGsDJ0V3Pf C07HD8VBk68TkH1HIBrfHs99NT1et/w521AUMtN6I+3V0anIClox/j2OuW12boGBCjPDKBbX mv5HgNh/EjPskH+esIVVxYBjqp9CPbNFc+/REMmqcv+gInoglka0wg+cebjgS3sFMOz078Qq 9V030UDOQ==
  • Ironport-hdrordr: A9a23:KALAl6EqzzSWNc5kpLqEFceALOsnbusQ8zAX/mt6Q3VuA7Glfq GV7Y4mPHrP4gr5N0tQ/uxoVJPwJU80sKQFhLX5Xo3SPzUO2lHYVb2KhLGKq1bd8m/Fh4xgPM xbAtBD4bPLfCNHpPe/zw+iDd46zdWLtIyuj/zP1mpgQGhRB51I3kNWDkK1HkVqWBJLH/MCZf yhz/sCiT7lV3p/VKqG77o+MNQrZeenqHsrW3877tcciDWzsQ==
  • Ironport-phdr: A9a23:sD4RyBCqUQLHKLmr1zgbUyQUI0oY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua43ygeRFt+Lsagew8Pt8IneGkU4oqy9+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiTSjbb9oM Bm6sQrdutcVjId8NKo91AbCr2dVdehR2W5nKlWfkgrm6Mu34JBt7Tlbteg7985HX6X6fqA4Q qJdAT87LW0759DluAfaQweX6XQSTmsZkhxTAwjY9x76RYv+sjH7tuVmxiaXO9D9QK0uVjSj6 6drTwLoiDsCOjUk/mzbltB8gaRGqx2muxFyzZLYbJyMOPZiY6/WYNcWSXdBU8pUUSFKH4GyY JYVD+cZMulYoYvyqVsAoxW9GAeiGv/gxyJTi3DswaE3yf4sHR3a0AEiGd8FrXTarM/yNKcXS e27yK7IzS7dYPNYxDzy5pLIfQs7rvGKQLl9dsjRyU40FwzbgFWcs5HlPymO2esXtWiW9OVgV ee1hG4mrwF9uCSgxsApioTQgI8e11/L+zljzokvOd24VFB0YcSiEJZIuCyWKpd7T988T2xou Ss21qAKtIC/cSQXyJoqxQDSZuKHfoWG/x/tVPicLDl6iX9lZr+yhRm8/FS9x+HhWMe5zFBHp TdLnNnLs3ACzR3T6s6fR/Rn/0ehxS6P2xnP5eFDJ0A0m7TUK4Q/zb42ipUcr17PHijsmEX5l KOZaF8r+vOo6uv7YrXpvJ6cN5VuhgH5KKQuldSzDvg+MggURGiX4+q81Kf78ULjRLVKkvw2n bLEsJDBP8gUuqm5AwpT340+6Bi/Fy+r3MoEkXQDNl5IexKKg5L3N13TL/30F+qzjlaonTpt2 vvLILnhAojWLnjfjrjhZ6tz609dyQUt1d1T+5RZAawbLv3pQE/+rtnYAwc5MwOqx+bnD81w1 oYEVmKOBq+VKbvSsVuV6u42LemAeY0YtTLnJ/gq4P7uinA5mVsDcqWzwZQXb3W4EuxnI0Wff 3Xsns8MHXkWsgc6VuDni12PXSRNa3qvUK8w/Cw3BYCiAIvbQ4Cimr2B3CO1Hp1MYWBGD0iBE XXvd4WfRfgMZjieItJ7kjMfT7ehTZQs1R6rtADgyrpnKvDY9TEftZLmzNR14fbcmgko9TNoF 8Sdz32NT2Zsk28VXzM2xrxwoVRhylef1qh1m+BXFdtK5/9QTgg6MYPcwPdhBtDpWgPBe8+JR 0y8TtWnBzExVNMxzMUUb0ZzAdXxxizEigitGLIb34GRDpUyuvb+2GP8KYBA0XzP0oEuilAnR o1EMmjw1YBl8A2GJYnSnkvRqrygfKJUiCzK72qNi3eUtkheeAF1WKTBG3sYYx2F/pzC+kreQ ur2WvwcOQxbxJvbd8OiC/XshFRCH7L4PcjGJnm2gyG2DAqJwbWFaMzrfX8c1WPTEhtMiBgdq FCBMwV2HSK9uyTGFjU7F1X0bk2q7PN0oXWTQUo9zgXMZEpkhPKu4hBAvfWHULsI264c/iIoq jF6BlG4itDRENeO4Rd7dqxaSdw46VZDk2nesl81JYSueoZlgFNWaAFrpwXu2hFwX51HitQvp Wg2wRBaLKuZ1BZZc2rd08mva/vYLW79+B3pYKnTsr3H+PCR/KpHqPExqlG4+RqsClJn6HJ/l d9cz3qb4JzOSgsUS5P4FEgtpVB8oPnBby8x6pmxtzUkOLSosjLEx9MiBfc0ghemcdBFNaqYF Qj0W8QEDsmqIeYulhCndBUBdOxV8ac1OYuheZ7kkOapO/1tknS7l25O5qhy10uN82x3TeuJl 5cJzveE3xeWAi/mhQTE0Ii/koRFaDcOW2unnHK8VcgBO+soJNpNUDj/cKjVjp1kipXgWmBV7 gumDlICg4qyfAaKKkf6xUtW3FgWpnqunW25ySZ1mncntPn6vmSGzuL8eR4AImMOSnNliAKmI 4+vgt5cQVKiZg4Bmx6s5EK8zK9e7vcaTSGbUQJTci76Ins3GKm3rbeMJdNV4poumSpSWeW4J 1udT/SuxnlSmzOmFGxYyjchcjissZishB12hlWWK3NrpWbYc8V9rfvGzOTVXuUZnj8PRS0jz CLSGkD5JN6xu9Odi5bEtOm6EWOnTJxaNyfxn8uMsy6y5GsiBhPa/bj7mNr8HAZ8zDXx3t9CW iDBrRK6aY7un6i3KuNoeEB0CUS0sZIrXNEj1NFp2NdJhilSj47d5XcdlGbvLdhXvMC2JGEAQ zIG2Z+d4QTo3lFiMmPcwov4UnuHxc4yL9K+Y24Qxmc895UQUPbSvOECx3Ip5APn/FG0A7A1h DoWxPow5WRPhugIvFFo1SCBGvUJGlEeOyXwlhOO5tT4raNNZW/pf6LjsSg21d2nEryGpRlRH XjjfZJ3Vy139chxdk/W2nT1wo7hcdjUK9kUs1fH9nWIx/gQM583mvcQ0GBlPnnwszs40eQyi zRh2Ji7uM6MLGAnr8fbSlZIczbyYc0U4DTki61Ty92X046YFZJkAjwXXZHsQKHgAHcIuP/gL QrLDCwkpyLRB+/EBQHGohQDzTqHA9WxOnqQPnVc0dhyWEzXOhlEmA5NFDQiwsxiS0bzlZSnK hsmoGhWvAKwqwMQmLw0cUOkCSGG+l/uMnBtGf39ZFJX9l0QuRmTaJTEqLo1R2YCptWgtFDfd DLdPVgZSzFRHBTDXQirP6Hyt4aatbHEQLPvdb2WJuzezI4WH/aQmcDwjs0/pWvKboPXeSA8R /wjhhgaBSA/QpuG3WVJE2tNzmrMd5LJ/UjnvHQm8obntqysAVyKh8PHCqMOY483qlbm3OHab b7W3GEgdn5Zzs9enyaWjuVPmgdD0Wc2MGD8WbUY6XyXFfyWwPQGSUVBLXs0bZotjep0yABJP YSzZsrd8Ll+g7Z1Dl5EUQekgcS1fYkRJHn7MlrbBUGNPbDAJDvRwsixb7nuAbtXxP5ZsRG9o 1P5WwfqIyiDmj/1VhuuLfAEjSeVOwZbsZ28dRAlAHbqTdbvYBm2eNFtijh+zboxj3LMfWkSV Fo0O1tKtaGV5DhEj+9XHmVA6j99KbDBlX/Gvq/XLZEZtfYtCSNx1qpb7Hk817pJ/XRESfhyy 06w5pZlp1CrlPXKyyIyCkIf7GYWwtjS4QM7ZvSKk/sIEWzJ9x8M82iKXhEDpt8+T8bqp7gV0 d/X0qT6NDZF9dvQu8oaHcndbsydYx9DeVLkHiDZCAwdQHulL2ba0gZfl+qf+DuItJIzrLDjn ZMPTvlQU1l/RZZ4Qgx1WccPJpt6RGZuibmAkMsB/maztjHUTcRe+4jDD7ecWKq+bjmeirZAa l0DxrayfuFxfsXrnkdlbFd9hoHDHUHdCMtMriNWZQgxuExR8XJ6QwXbPmrqbwqs5DkYEvvmx nbeayN7aOUpsS/ouhI5fwWb4iQ3l0Y1lJPuhjXDKFYZw4+/WIhXD2z/sE1ja/vG
  • Ironport-sdr: 681934c5_sqcykvHwPtzgfZSWS7CTK+626D+i0p/4/ZIyEbfp6yapGc1 kLKVecTIV51GBaMJ8b8D8CydvZqU3KrNbRFy6pA==

FINAL CALL FOR CONTRIBUTIONS - EXTENDED DEADLINE

Artificial Intelligence and Theorem Proving,
AITP 2025
August 31 - September 5, 2025, Aussois, France

http://aitp-conference.org/2025

Deadline: Extended to May 12, 2025
https://easychair.org/conferences/?conf=aitp2025

BACKGROUND
Large-scale semantic processing and strong computer assistance of
mathematics and science is our inevitable future. New combinations of
AI and reasoning methods and tools deployed over large mathematical
and scientific corpora will be instrumental to this task.  The AITP
conference is the forum for discussing how to get there as soon as
possible, and the force driving the progress towards that.

TOPICS

- AI, machine learning and big-data methods in theorem proving and mathematics.
- Collaboration between automated and interactive theorem proving, in
  particular their AI/ML aspects.
- Common-sense reasoning and reasoning in science, relations to general AI.
- Alignment and joint processing of formal, semi-formal, and informal
   libraries, Formal Abstracts.
- Methods for large-scale computer understanding of mathematics and science.
- Combinations of linguistic/learning-based and semantic/reasoning methods
- Formal verification of AI and machine learning algorithms, explainable AI .
 

SESSIONS

There will be several focused sessions on AI for ATP, ITP,
mathematics, relations to general AI (AGI), Formal Abstracts,
linguistic processing of mathematics/science, modern AI and big-data
methods, and several sessions with contributed talks. The focused
sessions will be based on invited talks and discussion
oriented. AITP'25 is planned as an in-person conference.


CONFIRMED PARTICIPANTS/SPEAKERS/PANELISTS (TBC)

João Araújo, Universidade Nova de Lisboa
Michael R. Douglas, Stony Brook University
Mario Carneiro, Chalmers University
Thibault Gauthier, Czech Technical University in Prague
Georges Gonthier, INRIA
Thomas C. Hales, University of Pittsburgh
Sean Holden, University of Cambridge
Jan Jakubuv, Czech Technical University in Prague
Mikoláš Janota, University of Lisbon
Moa Johansson, Chalmers University
Peter Koepke, University of Bonn
Konstantin Korovin, The University of Manchester
Michael Kinyon, University of Denver
Miroslav Olsak, University of Cambridge
Michael Rawson, University of Southampton, UK
Stephan Schulz, DHBW Stuttgart
Martin Suda, Czech Technical University in Prague
Josef Urban, Czech Technical University in Prague
Adam Vandervorst, Qoba.ai
Petr Vojtěchovský, University of Denver
Sean Welleck, Carnegie Mellon University
Zsolt Zombori, Alfréd Rényi Institute of Mathematics


CONTRIBUTED TALKS
We solicit contributed talks. Selection of those will be based on
extended abstracts/short papers of 2 pages formatted with easychair.cls.
Submission is via EasyChair (https://easychair.org/conferences/?conf=aitp2025).
The extended abstracts are considered non-archival.
The contributed talks have to be presented in-person.


DATES
Submission deadline: Extended to May 12, 2025
Author notification: June 20, 2025
Conference registration: TBA
Camera-ready versions: TBA
Conference: August 31 - September 5, 2025


PROGRAM COMMITTEE (TBC)

Michael R. Douglas (co-chair), Stony Brook University
Ulrich Furbach, University of Koblenz
Thibault Gauthier, Czech Technical University in Prague
Thomas C. Hales (co-chair), University of Pittsburgh
Sean Holden, University of Cambridge
Mikoláš Janota, University of Lisbon
Moa Johansson, Chalmers University
Cezary Kaliszyk (co-chair), University of Melbourne
Michael Kinyon, University of Denver
Konstantin Korovin, The University of Manchester
Mirek Olsak, University of Cambridge
Bartosz Piotrowski, IDEAS NCBR
Michael Rawson, University of Southampton, UK
Stephan Schulz (co-chair), DHBW Stuttgart
Sho Sonoda, RIKEN AIP
Martin Suda, Czech Technical University in Prague
Josef Urban (co-chair), Czech Technical University in Prague
Sean Welleck, Carnegie Mellon University
Zsolt Zombori, Alfréd Rényi Institute of Mathematics


LOCATION AND PRICE

The conference will take place from August 31 to September 5 2025
in the CNRS Paul-Langevin Conference Center
(https://www.caes.cnrs.fr/sejours/centre-paul-langevin/) located in
the mountain village of Aussois in Savoy.  Dominated by the "Dent
Parrachée", one of the highest peaks of La Vanoise, Aussois is located
on a sunny plateau at 1500 m altitude, offering a magnificent panorama
of the surrounding mountains and a direct access to the park of La
Vanoise in summer and downhill ski slopes or cross country slopes in
winter. The total price for accommodation, food and registration for
the five days will be around 600 EUR.

ARRIVAL/DEPARTURE

Aussois is less than 2h from the airports of Lyon, Geneve, Chambery,
Annecy, Grenoble and Turin. There are trains and buses from these
airports. Aussois is 7km from the Modane TGV station with direct
trains from/to Paris. We will organize a bus for the participants from
there to Aussois. Further buses to these airports / station can be
found at http://www.altibus.com/ .

ORGANIZERS
Georges Gonthier, Cezary Kaliszyk and Josef Urban


  • [Coq-Club] AITP 2025 FINAL CALL FOR CONTRIBUTIONS - EXTENDED DEADLINE May 12, Josef Urban, 05/05/2025

Archive powered by MHonArc 2.6.19+.

Top of Page