Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quanta Magazine article on an LLM for Isabelle

Email Gateway (Feb 17 2023 at 18:14):

From: Lawrence Paulson <lp15@cam.ac.uk>
Mentioning my colleague, Wenda Li

https://www.quantamagazine.org/to-teach-computers-math-researchers-merge-ai-approaches-20230215/?mc_cid=e8e39e38e1&mc_eid=b015f7100c

Larry

Email Gateway (Feb 17 2023 at 18:31):

From: Haniel Barbosa <hbarbosa@dcc.ufmg.br>
Both Tony Wu and Jason Rute (featured in the article) have given talks
this week in the Machine Assisted Proofs workshop at IPAM/UCLA on this
topic:

• Tony Wu, "Autoformalization with LLMs" https://youtu.be/_pqJYnQua58
  
• Jason Rute, "Deep Learning in ITP", https://youtu.be/P5ew0BrRm_I
  

The recordings of other talks in the workshop are in the IPAM channel,
btw: https://www.youtube.com/@IPAMUCLA/videos

Lawrence Paulson <lp15@cam.ac.uk> writes:

Email Gateway (Feb 20 2023 at 07:06):

From: Tobias Nipkow <nipkow@in.tum.de>
It seems to me that the most promising approach is to combine AI with a hammer,
as Tony Wu showed in his "formal sketches". It is similar to the combination of
neural networks and tree search that makes AlphaGo so powerful.

Tobias

smime.p7s

Last updated: Jan 04 2025 at 20:18 UTC