Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Month in Mathlib May 2024 #76

Merged
merged 14 commits into from
Jul 1, 2024
Merged

Month in Mathlib May 2024 #76

merged 14 commits into from
Jul 1, 2024

Conversation

YaelDillies
Copy link
Collaborator

No description provided.

grunweg
grunweg reviewed Jun 13, 2024
View reviewed changes
Copy link
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for writing this!!

I think the recent milestones towards the classification of Lie algebras would also be worth it - IIRC, they were mentioned on zulip as well?

posts/month-in-mathlib-may-2024.md Outdated Show resolved Hide resolved
PatrickMassot
PatrickMassot reviewed Jun 13, 2024
View reviewed changes
posts/month-in-mathlib-may-2024.md Outdated
<!-- TEASER_END -->

* Algebra
* [PR #13271](https://github.com/leanprover-community/mathlib4/pull/13271) :: chore(mathlib4/Algebra/BigOperators/Basic): unscope `∑ x ∈ s, f x` notations
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don’t understand why this is in the list. I’m happy about this PR, but it doesn’t seem worth mentioning.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's important to announce somewhere that open scoped BigOperators is now a no-op. Lean won't tell you.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Were there removed from Mathlib?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, they were removed in leanprover-community/mathlib4#13181.

Note that I now moved the above line from "Algebra" to "General library maintenance"

posts/month-in-mathlib-may-2024.md Outdated Show resolved Hide resolved
@YaelDillies
Copy link
Collaborator Author

The PRs are mentioned but I did not write a paragraph yet. I'm sure Oliver is more competent to write it than me.

riccardobrasca
riccardobrasca reviewed Jun 25, 2024
View reviewed changes
posts/month-in-mathlib-may-2024.md Outdated
* [PR #13347](https://github.com/leanprover-community/mathlib4/pull/13347) :: feat(NumberTheory/LSeries): special values of Hurwitz zeta
* [PR #13273](https://github.com/leanprover-community/mathlib4/pull/13273) :: feat(NumberTheory/LSeries): Riemann zeta as special case of Hurwitz
* [PR #12923](https://github.com/leanprover-community/mathlib4/pull/12923) :: feat (NumberTheory/Harmonic): compute Gamma'(1/2)
* Riccardo Brasca
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This can be removed, it is not interesting (of course the final proof will be!).

trivial1711
trivial1711 reviewed Jun 26, 2024
View reviewed changes
posts/month-in-mathlib-may-2024.md Outdated Show resolved Hide resolved
posts/month-in-mathlib-may-2024.md Outdated Show resolved Hide resolved
adomani
adomani approved these changes Jun 30, 2024
View reviewed changes
Copy link
Contributor

@adomani adomani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is awesome, thank you very much!

posts/month-in-mathlib-may-2024.md Outdated Show resolved Hide resolved
posts/month-in-mathlib-may-2024.md
* Miyahara Kō heroically ported the `cc` tactic to Lean 4: [PR #11956](https://github.com/leanprover-community/mathlib4/pull/11956), [PR #11960](https://github.com/leanprover-community/mathlib4/pull/11960) and [PR #5938](https://github.com/leanprover-community/mathlib4/pull/5938).
* Damiano Testa and Yaël Dillies replaced the `mk_all` shell script hardcoded to Mathlib with a Lean script that dynamically figures out the Lean libraries (sadly, Mathlib still needs some separate handling) in [PR #11853](https://github.com/leanprover-community/mathlib4/pull/11853), and [PR #11874](https://github.com/leanprover-community/mathlib4/pull/11874) made use of it in the "Check all files are imported" CI step. The script can now be used by any project downstream of Mathlib. If you maintain such a project, we encourage you to switch over to the new script and report eventual bugs.
* Vasily Nesterov implemented a simplex algorithm oracle in [PR #12014](https://github.com/leanprover-community/mathlib4/pull/12014). This is now the default oracle for `linarith` instead of the much slower Fourier-Motzkin oracle.
* [PR #13190](https://github.com/leanprover-community/mathlib4/pull/13190) and [PR #13293](https://github.com/leanprover-community/mathlib4/pull/13293) by Michael Rothgang and Damiano Testa neuters a very pernicious footgun: Contrary to expectations, `attribute [non_local_attribute] decl in` would **globally** tag `decl` with attribute `non_local_attribute`.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
* [PR #13190](https://github.com/leanprover-community/mathlib4/pull/13190) and [PR #13293](https://github.com/leanprover-community/mathlib4/pull/13293) by Michael Rothgang and Damiano Testa neuters a very pernicious footgun: Contrary to expectations, `attribute [non_local_attribute] decl in` would **globally** tag `decl` with attribute `non_local_attribute`.
* [PR #13190](https://github.com/leanprover-community/mathlib4/pull/13190) and [PR #13293](https://github.com/leanprover-community/mathlib4/pull/13293) by Michael Rothgang and Damiano Testa neuters a very pernicious footgun: contrary to expectations, `attribute [non_local_attribute] decl in` would **globally** tag `decl` with attribute `non_local_attribute`.

maybe? Although I see that the post has several occurrences of a capital letter after a colon, so maybe this is intended.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I slightly prefer capitalising after a colon since it is technically a new sentence starting

YaelDillies and others added 14 commits July 1, 2024 13:22
@YaelDillies
Script output
7f2bc55
@YaelDillies
Pick out the PRs mentioned in the thread
7eff37b 
I have singled out everything that was mentioned in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Month.20in.20Mathlib except for the import untangling of low level files.
@YaelDillies @ocfnash
@joelriou @grunweg
Paragraphs
9c1114a 
Co-authored-by: Oliver Nash <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
Co-authored-by: grunweg <[email protected]>
@YaelDillies @sgouezel
Sébastien's paragraph
5f3c921 
Co-authored-by: sgouezel <[email protected]>
@YaelDillies
Point to the correct repo in monthly-blog.sh
0badf78 
The script was still pointing to `mathlib` instead of `mathlib4`.
@YaelDillies
More sorting into subjects
58e15cb
@YaelDillies
Finish sorting
ac3d9bd
@YaelDillies @101damnations
Amelia's paragraph
849b294 
Co-authored-by: Amelia Livingston <[email protected]>
@j-loreaux @YaelDillies
write a blurb about the continuous functional calculus
d2252ed
@kim-em @YaelDillies
para on comonoids
80d912e
@YaelDillies @trivial1711 @loefflerd
David's and Mitchell's paragraphs
95c70b7 
Co-authored-by: Mitchell Lee <[email protected]>
Co-authored-by: David Loeffler <[email protected]>
@YaelDillies @ocfnash
Lie theory
ae52f37 
Co-authored-by: Oliver Nash <[email protected]>
@YaelDillies
polish
f271c3d
@YaelDillies @adomani
typo
a702f4d 
Co-authored-by: damiano <[email protected]>
@YaelDillies YaelDillies force-pushed the month-in-mathlib-2024-may branch from 9c6a099 to a702f4d Compare July 1, 2024 11:23
@YaelDillies YaelDillies merged commit 651f4e3 into master Jul 1, 2024
2 checks passed
@YaelDillies YaelDillies deleted the month-in-mathlib-2024-may branch July 1, 2024 11:28
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@trivial1711 trivial1711 trivial1711 left review comments

@101damnations 101damnations 101damnations left review comments

@joelriou joelriou joelriou left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

@dagurtomas dagurtomas dagurtomas left review comments

@PatrickMassot PatrickMassot PatrickMassot left review comments

@sgouezel sgouezel sgouezel left review comments

@grunweg grunweg grunweg left review comments

@ocfnash ocfnash ocfnash left review comments

@loefflerd loefflerd loefflerd left review comments

@adomani adomani adomani approved these changes

Assignees
No one assigned
Labels
WIP
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.