Lean good first issues

This issue describes Erdős Problem 784, which asks whether a subset A of {1,...,n} with a bounded sum of reciprocals (sum(1/a for a in A) <= C) guarantees the existence of a constant c such that the count of numbers <= n not divisible by any element of A is at least n/(log n)^c. The problem is marked as solved and is up for grabs.

This issue proposes adding a `nodup` assumption to the `Enumeration` type class in the `veil-dev` project. This assumption would guarantee that the `allValues` list for an enumerated type contains no duplicates, potentially leading to performance improvements in certain scenarios like `ExtTreeMap` computations. The change involves modifying the `Enumeration` class definition and ensuring existing instances are compatible or updated.

An AI agent found a disproof for the Bateman-Horn Conjecture in Lean, but it's likely due to a misformalization of the Bateman-Horn constant. The issue lies in the use of an unconditional infinite product (`tprod`) which evaluates to a junk value (0 or 1) when the product is only conditionally convergent. This leads to incorrect constant values, enabling the disproof.

This issue identifies a potential misformalization in a statement from Erdos problems regarding the density of integers of a specific form. The current phrasing uses "density" which might be interpreted as natural density, but the suggested fix is to explicitly bound the lower density instead. This aims to clarify the mathematical statement's intent.

This issue proposes adding Green's Open Problem #6 to the repository, which asks for the size of the largest sum-free subset of the d-dimensional hypercube [N]^d. The problem is currently open and is seeking contributions from the community.

This issue aims to formally implement a low-rate capacity-achieving Reed-Solomon list decoding algorithm based on a specific research paper. The formalization involves four distinct technical areas: Hasse-Taylor algebra, interpolation spaces, anisotropic simplex/lattice estimates, and a differential-equation solver. The project emphasizes parallel development with frozen interfaces and small, clean pull requests.

The `deriving` mechanism in Lean 4 does not correctly handle `unsafe` attributes, preventing its use with `unsafe` code. The issue proposes that `deriving unsafe Repr, unsafe BEq` could be a potential solution, or that the system should error deliberately to prevent accidental unsafe code generation.

This issue requires a formal mathematical proof within a formal verification system (likely Lean) of the Glosten-Milgrom adverse-selection model. The proof should demonstrate how the bid-ask spread arises from informed traders and Bayesian updating, and confirm that the spread is positive under specific conditions. This involves implementing Bayesian probability and conditional expectations.

This issue proposes adding support for the `hw.instance` operation in CIRCT, which is necessary for instantiating previously defined `hw.module` operations. The implementation will involve defining a new operation and verifier within Veir's HW dialect, with initial support focusing on core functionality and ignoring `inner_sym` and `doNoPrint` parameters.

This issue proposes a strategy to process 251 specific routines that are loop-free but contain function calls. The approach involves composing existing contracts of called functions and then creating a prioritized worklist for parallel processing. Routines with un-contracted callees will contribute those missing contracts back to the work queue.

This issue proposes adding support for CIRCT's `verif.assume` and `verif.assert` operations to the Veir dialect. This involves creating a new `Verif` directory and defining the necessary operations and verifiers, initially focusing on cases where the property argument is an `i1`.

This issue proposes adding support for CIRCT's `seq` dialect within the Veir project. The initial goal is to implement parsing for the `seq.clock` type and the `seq.to_clock` and `seq.firreg` operations, enabling the representation of basic register circuits. Future enhancements include support for `seq.clock_inv` and `seq.shiftreg` operations.

This issue proposes to fix scoped notation for topological properties (like `IsOpen[T]`) so that they are correctly displayed in documentation generation. Currently, this notation is not rendered, making it difficult to understand the specific topology used in certain mathematical definitions within the documentation.

This issue proposes the creation of an API map for Lattice Quantum Field Theory (QFT). The goal is to document the primary results and functionalities that should be included in this API map.

This issue proposes creating a new top-level directory named 'LatticeQFT' within the repository. This directory will serve as a foundational stub, containing a 'Basic.lean' file that will later reference other directories related to Lattice Quantum Field Theory. The goal is to establish a central point for organizing and linking future Lattice QFT work.

This issue tracks the development and formal security proofs for Merkle trees, a fundamental commitment scheme. The goal is to prove completeness, extractability, and hiding properties, which are non-trivial and require significant effort. Progress depends on foundational work in related issues, and specific tasks include defining openings, proving completeness for single and batch indices, and developing extractability and hiding proofs.

This issue requires the creation of semantic specifications (spec triples) for seven RLP read routines in Lean. While string-to-program correspondence theorems exist, the actual computation of these routines is not yet defined. The encode side routines are considered higher value and can be addressed independently.

This issue reports an incorrect symbol `𝓢` used in the documentation of the `physlib` repository. The symbol appears to be a typo and should be `𝓣` (time-ordering) to accurately reflect the mathematical content of the lemma `timeOrder_eq_maxTimeField_mul_finset`. The suggested correction replaces the erroneous symbol with the correct one for clarity and consistency.

This issue reports a typo in the `physlib` documentation where a tensor product example incorrectly refers to an undefined variable `T1` instead of the declared tensor `T`. The suggested correction replaces `T1` with `T` to align the example with the surrounding text and maintain consistency with other documentation in the file.

The documentation in `Position.lean` incorrectly states that a section discusses generalized eigenvectors of the momentum operator. The actual content, specifically the lemma `positionStates_generalized_eigenvector_positionOperatorUnbounded`, demonstrates that these are generalized eigenvectors of the position operator. The suggested correction is to change the documentation header to accurately reflect this.

The documentation for a mapping function in the `physlib` repository incorrectly claims that anomaly cancellation is preserved. Upon investigation, there are no lemmas or proofs in the associated code that support this claim, while other documented properties like potential term presence and completeness are indeed supported. The suggested correction removes the erroneous claim about anomaly cancellation from the documentation.

The documentation for the `Renyi.lean` file incorrectly claims it covers α-Renyi entropy. Upon inspection, the file only contains definitions and theorems related to quantum relative entropy, with no mention or implementation of α-Renyi entropy. The suggested correction is to remove the false claim from the module docstring.

The documentation for `normPowerSeries` incorrectly identifies it as a power series. The issue points out that its definition `sqrt(‖x‖^2 + 1/(n+1))` is a sequence of functions, not a power series. The suggested correction replaces "power series" with "sequence of functions" to accurately reflect its mathematical nature.

The documentation for `realLorentzTensor` in `Basic.lean` incorrectly states it's for complex Lorentz tensors. The surrounding code and context clearly indicate it's for real Lorentz tensors, and the suggested correction updates the docstring to accurately reflect this.

The documentation for the Euler-Lagrange equations in the `physlib` repository incorrectly states that the variational derivative of the Lagrangian itself is equal to the `eulerLagrangeOp`. The actual theorem proves that the variational derivative of the action functional (the integral of the Lagrangian over time) yields the Euler-Lagrange operator. The suggested correction clarifies this by referring to the integral of the Lagrangian.

The documentation for the MSSM in the `physlib` repository incorrectly claims support for right-handed neutrinos (RHNs). The actual code implements anomaly cancellation conditions only for the standard MSSM without RHNs, lacking any definitions for RHN-specific species or charges. The suggested correction removes the mention of RHNs from the documentation to align it with the code's capabilities.

The documentation for Lorentz tensors in `Metrics/Basic.lean` incorrectly labels them as 'complex' when they are actually real-valued, as indicated by the `ℝT` type. The suggested correction is to change 'complex' to 'real' in the documentation to accurately reflect the tensor's type and mathematical context.

This issue reports a documentation error in the `physlib` repository regarding the Levi-Civita tensor. The current documentation incorrectly states that `ε4` represents a rank-four Levi-Civita tensor in 3-dimensional space. The actual tensor is rank-three and exists in 4-dimensional space, as indicated by the code's use of `Fin 4` indices.

The documentation for WickAlgebra grading in `Grading.lean` incorrectly states that the parameter `𝓕` is a `FieldStatistic`. In reality, `𝓕` is a `FieldSpecification`, which is a structure containing field data. The documentation should be updated to reflect this distinction to avoid confusion between the grading group (`FieldStatistic`) and the parameter's type.

The documentation for the Galilean action on space in `physlib/Physlib/SpaceAndTime/GalileanGroup/Basic.lean` incorrectly states it acts on space at a fixed time. The function `actSpace` actually depends on a `Time` parameter `t`, as shown in its implementation and the module's definition of Galilean transformations. The suggested correction clarifies that the action depends on the given time `t`.