Zulip Chat Archive

Also see #announce > NASEM virtual workshop: AI to Assist Mathematical Reasoning . But this stream is the best place on Zulip to discuss the workshop, since discussion in the announcements stream is discouraged.

Lars Ericson (Jun 02 2023 at 23:23):

I heard about it from https://terrytao.wordpress.com/2023/06/02/ai-to-assist-mathematical-reasoning-a-workshop/

Lars Ericson (Jun 05 2023 at 10:49):

What an AI model needs to represent depends on the tasks you expect the model to perform.
An LLM might have to ingest the Lean concept hierarchy, which is reflected in the import hierarchy of the core Lean library
Screenshot-from-2023-06-05-06-28-39.png
and mathlib on top of that
Screenshot-from-2023-06-05-06-29-14.png

Eric Wieser (Jun 05 2023 at 13:29):

That's the file import hierarchy, certainly not a "concept hierarchy"

Lars Ericson (Jun 06 2023 at 00:42):

It's a visualization. Each file is organized around a particular set of ideas and facts. The visualization gives an impression of what ideas are required to express other ideas, and also an sense of density of ideas. The Lean core library is pretty dense but can fit on a page. Mathlib is much more dense and the imports would require 5 or 10 pages to print out legibly. The imports go all over the place, as shown in the picture, so that one collection of ideas might depend on quite a few other upstream ideas. I'm not sure what people expect of an AI model. One expectation might be that it can encode all of these relationships, which Lean already does when it reads in the library, so I'm not sure what other things people might expect beyond that. I'll find out at the conference.

Jason Rute (Jun 12 2023 at 17:45):

Talia Ringer is live tweeting their thoughts on the workshop if anyone is interested: https://twitter.com/TaliaRinger

Jason Rute (Jun 13 2023 at 16:13):

Talia's Day 2 Thread: https://twitter.com/TaliaRinger/status/1668626243108106240

Kaiyu Yang (Jun 16 2023 at 06:33):

Does the workshop have video recordings?

Kevin Buzzard (Jun 16 2023 at 06:52):

I asked about this and was told that they will appear online at some point

Siddhartha Gadgil (Jun 16 2023 at 08:53):

The first two days' recordings are at https://vimeo.com/831642504 and https://vimeo.com/831621752 for the AI for Mathematics

Johan Commelin (Jun 16 2023 at 10:12):

Apparently you need a vimeo account to watch these

Scott Morrison (Jun 16 2023 at 10:20):

Accounts are free, although it takes a moment to find the "no thanks" link at the point they ask you for money.

Junyan Xu (Jun 16 2023 at 15:23):

The third day: https://vimeo.com/831643416

Alex Kontorovich (Jun 16 2023 at 18:41):

I posted my slides/notes here: https://twitter.com/AlexKontorovich/status/1669765302735831043?s=20 Happy to hear suggestions/criticisms etc!...

Adam Topaz (Jun 16 2023 at 19:21):

Johan Commelin said:

Apparently you need a vimeo account to watch these

it seems that I can watch the videos without an account...

Adam Topaz (Jun 16 2023 at 19:21):

Anyway, here are my slides, in case anyone finds them useful:
pres.pdf

Oisin McGuinness (Jun 16 2023 at 20:32):

Alex, thanks for a great talk, and for posting these notes.
Here's a direct link to your talk in the Vimeo video: https://vimeo.com/831643416#t=2h17m08s

Alex Kontorovich (Jun 16 2023 at 22:18):

Oh great, thanks!

Lars Ericson (Jun 17 2023 at 19:22):

At some point in the AI in Math conference, someone mentioned an introductory category theory in Lean tutorial by Carlo Angiuli. I didn't find that in Youtube or elsewhere, did I hear wrong?

I looked at this video by @Johan Commelin on the Liquid Tensor Experiment. Around 1:15:09 he says "we're not actually doing the internal logic of a category which is frustrating but we're still able to take regular formulas and interpret them and simplify parts of the proof that way".

As a measure of "practical category theory impact", one could add up how many of the 100,000 or so theorems in Lean 3 depend either directly or indirectly on imports to mathlib/src/category. Just using grep I saw references in homology, algebraic geometry, algebraic topology, analysis, combinatorics, group theory, logic, model theory, representation theory, ring theory and topology. Excluding sections of those topics that define categories within those areas which are not subsequently used elsewhere, intuitively I guess that 1% to 5% of the 100,000 have a dependency on category theory. It would be nice to see an exact number, and also a view on what this percentage should be.

Here are the direct references I found with grep:

algebra.homology.Module
algebra.homology.additive
algebra.homology.differential_object
algebra.homology.homological_complex
algebra.homology.homology
algebra.homology.homotopy_category
algebra.homology.image_to_kernel
algebra.homology.quasi_iso
algebra.homology.short_exact.abelian
algebra.homology.short_exact.preadditive
algebra.module.injective
algebra.module.pid
algebraic_geometry.AffineScheme
algebraic_geometry.Gamma_Spec_adjunction
algebraic_geometry.Scheme
algebraic_geometry.locally_ringed_space.has_colimits
algebraic_geometry.morphisms.basic
algebraic_geometry.open_immersion
algebraic_geometry.presheafed_space
algebraic_geometry.presheafed_space.has_colimits
algebraic_geometry.projective_spectrum.topology
algebraic_geometry.properties
algebraic_geometry.pullbacks
algebraic_geometry.ringed_space
algebraic_geometry.stalks
algebraic_geometry.structure_sheaf
algebraic_topology.Moore_complex
algebraic_topology.alternating_face_map_complex
algebraic_topology.cech_nerve
algebraic_topology.dold_kan.gamma_comp_n
algebraic_topology.dold_kan.n_reflects_iso
algebraic_topology.dold_kan.p_infty
algebraic_topology.dold_kan.projections
algebraic_topology.fundamental_groupoid.basic
algebraic_topology.fundamental_groupoid.fundamental_group
algebraic_topology.fundamental_groupoid.induced_maps
algebraic_topology.fundamental_groupoid.product
algebraic_topology.fundamental_groupoid.punit
algebraic_topology.fundamental_groupoid.simply_connected
algebraic_topology.simplex_category
algebraic_topology.simplicial_object
algebraic_topology.simplicial_set
algebraic_topology.split_simplicial_object
algebraic_topology.topological_simplex
analysis.normed.group.SemiNormedGroup
analysis.normed.group.SemiNormedGroup.completion
analysis.normed.group.SemiNormedGroup.kernels
combinatorics.hall.basic
group_theory.nielsen_schreier
logic.small.list
model_theory.bundled
representation_theory.Action
representation_theory.Rep
representation_theory.fdRep
representation_theory.group_cohomology_resolution
ring_theory.ring_hom_properties
topology.gluing
topology.sheaves.abelian
topology.sheaves.forget
topology.sheaves.limits
topology.sheaves.locally_surjective
topology.sheaves.operations
topology.sheaves.presheaf
topology.sheaves.presheaf_of_functions
topology.sheaves.sheaf
topology.sheaves.sheaf_condition.equalizer_products
topology.sheaves.sheaf_condition.pairwise_intersections
topology.sheaves.sheaf_condition.sites
topology.sheaves.sheaf_condition.unique_gluing
topology.sheaves.stalks

Oisin McGuinness (Jun 17 2023 at 19:31):

Hi Lars, regarding the Carlo Angiuli reference, perhaps the videos in his playlist https://www.youtube.com/playlist?list=PL5s3lB5-wPG2xqV_krdsR6VnBciHDZ8Fz (linked from his home page https://www.cs.cmu.edu/~cangiuli/ )are intended.

Kevin Buzzard (Jun 17 2023 at 22:08):

The exercises for LFTCM2020 contain a section on category theory in mathlib3.

Kevin Buzzard (Jun 17 2023 at 22:10):

Here is the source code for the exercises.

Junyan Xu (Jun 18 2023 at 04:16):

Terry Tao got access to GPT-4 and his article based on the interactions was just published by Microsoft: https://unlocked.microsoft.com/ai-anthology/terence-tao/

Strangely, even nonsensical LLM-generated math often references relevant concepts. With effort, human experts can modify ideas that do not work as presented into a correct and original argument. The 2023-level AI can already generate suggestive hints and promising leads to a working mathematician and participate actively in the decision-making process. When integrated with tools such as formal proof verifiers, internet search, and symbolic math packages, I expect, say, 2026-level AI, when used properly, will be a trustworthy co-author in mathematical research, and in but many other fields as well.

[emphases mine]