From Sets in Math to Types in Lean: Subtype, Fin, Finset ...

Stream: new members

[Rado Kirov]

I wrote a blog post based on my experience formalizing statements from Tao's Analysis I

From Sets in Math to Types in Lean: Subtype, Fin, Set, Finset, and Fintype

It is aimed towards Lean newcomers (like myself). Since I have no comments on the blog, I am posting it here for a possible discussion, comments, etc.

Note: AI was used to generate and edit some of the blog text.

[Wrenna Robson]

@Rado Kirov Some comments:

• Fin n is actually technically not a subtype - I mean it is clearly equivalent to one but it isn't constructed that way!
• I found your writing style a little terse at points - I don't know if you used an LLM for drafting but it reads a bit like that to me, and it gives quite angular thought trains. I don't particularly enjoy this but others might.
• I think there's a lot more you can say about Finset. While it's mostly correct to use API to construct them, I think it would be useful in your exposition to understand how they are (equivalent to) a subtype of Multiset, and how Multiset is a quotient of List.
• S : Finset U and Fintype S are more similar than you think - I don't think this is a good full exposition of the options. You can also use the Finite typeclass and the FinEnum typeclass - these could be good alternatives to Fintype. If S naturally sits in some other ambient type, we could have it as a Set, and then we could use the Set.Finite predicate (which is, under the hood, Finite ↥S. I think you really do not have a clear picture here.
• You say at one point that is is generally better to use ∈ S in sums, but in your example it's the opposite - which is it?
• I actually think your example is not perfect. Consider this: why do you index, in E, by Fin n? You do not use the ordering that exists on Fin n, after all: not in the statement, anyway. I think you only really need decidable equality on it. You could instead index by a finite type. I also do not see why S has to be a Fintype - indeed this feels quite unnatural to me. I would expect such an f to quite often be defined on the wider type S is a subset of! There's no use of union in your statement. This theorem is actually Finset.sum_biUnion, I think - go look at that!
• I agree with your overall conclusion but your example is partial, and I would not say personally wholly correct.

[Rado Kirov]

Thank you for the careful reading and critique!

Indeed, I used Claude code both to learn about the concepts in the post and write the post based on my rough draft and editorial direction. My personal unedited style is too rambly and rough, while Claude leans too much on writing short sentences, but cleans up my mess very quickly. Not sure which one is worse. Maybe I should experiment with leaving both versions :/

• will fix the Fin n in correctness. Thanks, I should have checked that one.
• not sure if I can add more to already quite long post about connections with Multiset, but something I will need to explore more myself.
• explicit Finite hypothesis as an alternative is a great suggestion will try to work it in. FinEnum I didn't even know it exists, need to learn more about it.
• the example uses ∑ s, f s = ∑ i, ∑ s ∈ E i, f s so there is one implicit s : S and one explicit s ∈ E i. The point is that if one naively write s : E i they will be in trouble. I know to an expert that is obviously a disaster, but to a newcomer it feels like an easy mistake.
• Indexing by Fin n is actually a recent change I made because I thought it matches the style of the text best. It used to be :

/-- Exercise 7.1.6 -/
theorem sum_union_disjoint {X S : Type*} [Fintype X] [Fintype S]
    (E : X → Finset S)
    (disj : ∀ i j : X, i ≠ j → Disjoint (E i) (E j))
    (cover : ∀ s : S, ∃ i, s ∈ E i)
    (f : S → ℝ) :
    ∑ s, f s = ∑ i, ∑ s ∈ E i, f s

I take this version would be the one you will recommend I upstream in https://github.com/teorth/analysis/pull/448 (inspired by https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/BigOperators/Group/Finset/Basic.html#Finset.sum_biUnion with ℝ instead of M)

theorem sum_union_disjoint {ι κ: Type*} {f : ι → ℝ} [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} (hs : (↑s).PairwiseDisjoint t) :
∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i

While it feels it is the most general for the purpose of mathlib, it feels the most magical and mysterious to a newcomer - one has to know biUnion, there is an coersion (↑s) that I don't understand why at glance, and t is defined over all k not just s, so I am not sure I would say that would be the best translation for the purposes of the textbook companion.

[Snir Broshi]

Rado Kirov said:

Indeed, I used Claude code both to learn about the concepts in the post and write the post based on my rough draft and editorial direction.

Can I please ask that in the future if you post a link to AI output that you indicate it in the post? IIUC you asked for human feedback, which means you're asking for humans to read LLM output without indicating it as such.
(also I'm not sure posting AI blog posts is allowed here, but idk)

[Rado Kirov]

Sure, I added a disclosure - "AI was used to generate and edit some of the blog text."

Judging by your comment (and the AI slop threads) it seems that there is a lot of binary thinking - one either rejects AI fully or adopts it blindly and generates slop. You labelled the whole thing "AI blog post" and wonder if it should even be posted, while I believe it should be seen as the result of "AI-human" collaboration. There is a lot of subtlety between the extremes and some true productivity gains will be lost if all AI collaborations are rejected outright.

I hope you can tell from the post and the discussion I am having above that this post is based on my personal journey of working with Lean, based on my personal struggles on how to formalize a simple math statement and finding multiple correct and incorrect versions. Using AI to teach me the differences and deciding myself which one I believe is best to contribute upstream. I decided that other might benefit from reading about these basic Lean types. I have read every word and it is was written based on my direction.

It is objectively much faster for me to say "tighten my prose", "move this example", "add a section about subtypes in the context of sets", and get reasonable results. Nothing is fully free and I realize that the cost is producing slightly mechanical voice and "angular thought trains" as @Wrenna Robson said, but I cherish the fact that I could get this whole post out in one quick hour, while I get to do enjoy the rest of my vacation with my family. It saved me probably extra 2-3 hours of laborious editing.

No AI was used in writing the above. Arguing with people on the internet, the last remnant of a purely human activity ;)

[Rado Kirov]

And just to add - I empathize with the readers frustration with feeling deceived into reading something that was the product of a simple prompt "write me a blog post on sets vs types" and plopping the output here without any editing or further directions. But my post is not that.

[Wrenna Robson]

@Rado Kirov for what it's worth while AI stuff does often annoy me a bit I understand your use of it here and personally find it pretty benign. I don't have time right now to read all your reply but I'm really glad my critique was useful. Have a lovely evening.

[Snir Broshi]

Thank you for adding the disclosure!
I appreciate the nuances and did not 'reject your post as slop', but I believe the best policy is to put all the cards on the table upfront and let the reader judge for themselves, alleviating any possible deception as you mentioned. This matches with Mathlib's policy on PRs (#mathlib4 > policy proposal: mention AI use in PR description? @ 💬) where a similar nuance was pointed out.

[Rado Kirov]

but I believe the best policy is to put all the cards on the table upfront

Agree, will do!

[suhr]

It is objectively much faster for me to say "tighten my prose", "move this example", "add a section about subtypes in the context of sets", and get reasonable results.

But people are very good at recognizing things and can't stop notice AI tampering.

There's a way to workaround this: use AI only as an example generator and don't let it write the final result. Retyping the text gives you an opportunity to rephrase it.

[suhr]

I'm a terrible writer myself, and I found a different way to compensate this: I completely rewrite my text several times, alternating between typing and handwriting. For some reason handwriting helps me writing human-readable text, but typed text is easier to see as a whole.