experiment: hammer/premise selection benchmarks #106
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
kim-em
force-pushed
the
hammer_measurements
branch
3 times, most recently
from
5ae212a to
b1793a3
Compare
kim-em
force-pushed
the
hammer_measurements
branch
from
2012f87 to
e0a6b41
Compare
…mmunity#31520) This PR ensures we only have a single H1 header per lean file in the `Geometry` subdirectory. We do this for the following reasons: - Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting documentation webpage actually is. - The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3.
…er-community#31522) This PR ensures we only have a single H1 header per lean file in the `LinearAlgebra` subdirectory. We do this for the following reasons: - Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting documentation webpage actually is. - The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3.
…eanprover-community#31658) This PR ensures we only have a single H1 header per lean file in the `RepresentationTheory` subdirectory. We do this for the following reasons: - Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting documentation webpage actually is. - The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3.
…-community#31659) This PR ensures we only have a single H1 header per lean file in the `Probability` subdirectory. We do this for the following reasons: - Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting documentation webpage actually is. - The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3.
This PR adds a deprecation to the file `Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog`, which was moved to its own folder in leanprover-community#31626.
…ommunity#30567) This is the start of a series of PR aiming to prove two theorems related to partition: - [Glaisher's theorem](https://en.wikipedia.org/wiki/Glaisher%27s_theorem), which is a generalization of the existing [Euler's Partition theorem](https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean). The proof will use the infinite generating function, upgrading the current proof that uses finite ones, and resolving this [TODO](https://github.com/leanprover-community/mathlib4/blob/master/Archive/Wiedijk100Theorems/Partition.lean#L66) - [Pentagonal number theorem](https://en.wikipedia.org/wiki/Pentagonal_number_theorem) and the recurrence relation on the partition function. I created a new file `Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean` to avoid importing PowerSeries stuff directly into the definition file, and along the way I moved the existing `Mathlib/Combinatorics/Enumerative/Partition.lean` to `Mathlib/Combinatorics/Enumerative/Partition/Basic.lean` .
…anprover-community#31625) Current naming is confusing, `innerSL_apply` means `innerSL x y` but `innerSL_apply_coe` means `⇑(innerSL x)`...? So this PR renames these (and others). Renames: `Analysis/InnerProductSpace/LinearMap`: - `innerₛₗ_apply_coe` -> `coe_innerₛₗ_apply` - `innerₛₗ_apply` -> `innerₛₗ_apply_apply` - `innerₗ_apply` -> `innerₗ_apply_apply` - `innerSL_apply_coe` -> `coe_innerSL_apply` - `innerSL_apply` -> `innerSL_apply_apply` - `innerSLFlip_apply` -> `innerSLFlip_apply_apply` - `innerSL_real_flip` -> `flip_innerSL_real` `Analysis/InnerProductSpace/Dual`: - `InnerProductSpace.toDualMap_apply` -> `InnerProductSpace.toDualMap_apply_apply` - `InnerProductSpace.toDual_apply` -> `InnerProductSpace.toDual_apply_apply`
Adds a constructor for building affine equivalences from linear equivalences and base points.
…y#31684) The referenced lemma used to assume that both `f` and its Fourier transform are Schwartz functions, but this is no longer the case because we have the Fourier transform as a continuous linear map on Schwartz functions.
I am happy to remove some nolints for you! [workflow run for this PR](https://github.com/leanprover-community/mathlib4/actions/runs/19397459427) Co-authored-by: leanprover-community-bot <[email protected]> Co-authored-by: Bryan Gin-ge Chen <[email protected]>
…prover-community#31103) ... using properties of 2-connected components. From the ProofBench workshop
…er-community#31423) This PR ensures we only have a single H1 header per lean file in the `Combinatorics` subdirectory. We do this for the following reasons: - Having more than one H1 header per file is likely to hamper both assistive technologies and SEO, since it introduces ambiguity about what the title of the resulting documentation webpage actually should be. - The [documentation style guide](https://leanprover-community.github.io/contribute/doc.html) asks for the title of the file to be H1, any other header in the file-level docstring to be H2, and sectioning headers to be H3. I have used my own judgement to decide whether to demote the extra H1 headers to H2 or H3. I've also tried to ensure that any intended header hierarchy is maintained, by further demoting existing H2 comments to H3 where applicable. I ask reviewers to verify that my choices makes sense to them.
The current step using `git fetch` exits with a nonzero exit code if the branch is missing; `git ls-remote` will just return an empty string instead. It's used in two workflows so I fixed it in both places. (the branch used in `update_dependencies.yml` is protected from being deleted so we never noticed this issue) cf. https://github.com/leanprover-community/mathlib4/actions/runs/19384254316/job/55468689653
After [batteries#1486](leanprover-community/batteries#1486) is merged: - [x] Edit the lakefile to point to leanprover-community/batteries:main - [x] Run lake update batteries - [x] Merge leanprover-community/mathlib4:master - [ ] Wait for CI and merge Co-authored-by: leanprover-community-mathlib4-bot <[email protected]> Co-authored-by: F. G. Dorais <[email protected]>
Found and fixed with help from Codex.
…leanprover-community#31464) Let $A$ be an $R$-algebra for a commutative ring $R$ and $f:M\to N$ an $A$-module homomorphism. Given a derivation $D\in Der_R(A,M)$, we have a derivation $f \circ D$ of $Der_R(A,N)$. The induced map $Der_R(A,M)\to Der_R(A,N)$ is $A$-linear but was only reported to be $R$-linear in the previous implementation. All changes are in the PushForward section of the RingTheory/Derivation/Basic.lean file. The statements of definitions * `_root_.LinearMap.compDer` * `llcomp` * `_root_.LinearEquiv.compDer` are changed from $R$-linear to $A$-linear. For the stronger linearity the proof of `map_smul'` in `_root_.LinearMap.compDer` had to be changed. The rest remains as is. Edit: Some files explicitly used the weaker version, these have now been changed, by applying `.restrictScalars (R:=...)`, whereever the weaker linearity version of `compDer` was needed. Co-authored-by: leo <[email protected]>
…verages (leanprover-community#31583) Deliver on an open TODO and describe the logarithmic counting function in terms of circle averages. This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. The material established here is a step towards Cartan's classic formula for the Nevanlinna characteristic.
…over-community#29512) We ignore draft PRs and PRs with the WIP label. The set of checks is intentionally kept small, and could be expanded in the future. Co-authored-by: Bryan Gin-ge Chen <[email protected]>
…ommunity#31149) We add that the power series ring over a noetherian ring is noetherian.
…Homs` (leanprover-community#31298) In this PR, we build every API of the module version `IsAdicComplete.lift` for the ring version `IsAdicComplete.liftRingHom`. Mainly copying APIs in leanprover-community#25927, leanprover-community#31295, leanprover-community#31296. This would be used in leanprover-community#26388. Co-authored-by: Jiedong Jiang <[email protected]>
…rothendieck (leanprover-community#30071) Continuing from leanprover-community#29681, dualize all definitions and lemmas in the namespace `Pseudofunctor.CoGrothendieck` to results in the namespace `Pseudofunctor.Grothendieck`. - [x] depends on: leanprover-community#29681 Co-authored-by: jlh18 <[email protected]>
…#31166) Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
…-community#31793) Adds the theorem `MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconj`, showing that the ergodicity property can be pushed along a semiconjugacy.
…prover-community#30727) In this file, we show that if `κ : Cardinal.{u}` is a regular cardinal, then `X : Type u` is `κ`-presentable in the category of types iff `HasCardinalLT X κ` holds.
Restores lemmas in Mathlib.Combinatorics.SimpleGraph.FiveWheelLike that had been commented out during nightly testing, but which now build again (unmodified).
This has been forgotten in leanprover-community#31149.
…tions,Shapes}.Equalizers}` and `CategoryTheory.Subobject.Lattice` (leanprover-community#31784)
…-community#31608) This PR fixes `isUserFriendly`, in `unfold?`, for two reasons: - We should only worry about bad constants in the expression if they appear in the visible part of the expression. They should be allowed in e.g. instance implicit arguments. - We don't want to get raw projections, because these are generally not what we want to work with.
…nprover-community#31814) The workflow is being skipped on PR edits at the moment and being triggered on edits to the title by bors. This PR fixes both of those issues and some others found during testing.
…y#25856) We try to see what happens if we make Real.sqrt irreducible. There are cases where this makes unification very significantly faster, compare [#mathlib4 > Coercion triggers timeout @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Coercion.20triggers.20timeout/near/517177117). (Migrated manually from leanprover-community#24752)
…etion.RingHom (leanprover-community#31822) This was missed in leanprover-community#31149. Found by the linter in leanprover-community#31820.
…y#31827) The substitution with `${{ }}` breaks when the PR labels object has multiple lines. cf. [error](https://github.com/leanprover-community/mathlib4/actions/runs/19515906969/job/55867457030#step:4:49) caused by [malformed script](https://github.com/leanprover-community/mathlib4/actions/runs/19515906969/job/55867457030#step:4:11 )
…#31709) This PR tags the content of `Mathlib.Order.Defs.LinearOrder` with `@[to_dual]`. For this to work, we also tag some lemmas used by `grind` with the `@[to_dual]` tag.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.