Lean good first issues

This issue proposes formalizing the Hull-White (extended-Vasicek) bond pricing formula in Lean. The task involves deriving the bond price P(0,T) = A(T) * exp(-B(T) * r0), where B(T) is the same as in the Vasicek model and A(T) incorporates the time-dependent mean term and variance. The goal is to implement this in Lean, ensuring it's mathematically sound and integrates with existing code.

This issue aims to derive the prices of up-and-in and up-and-out binomial barrier options for a general terminal payoff. It builds upon existing proofs of the reflection principle and related combinatorial identities. The task involves splitting terminal positions at the barrier and utilizing the reflection principle to calculate prices, with an optional extension to non-symmetric trees and lookback payoffs.

This issue requires proving a mathematical identity relating the Radon-Nikodym derivative of a numeraire measure to its density function. Additionally, it involves updating documentation to point to a specific implementation of forward measures in the codebase.

This issue proposes formalizing key-rate (partial) duration in a financial modeling library. It involves defining the sensitivity of a bond's price to changes in specific spot rates and proving that the sum of these key-rate durations equals the effective duration under a parallel yield curve shift. This extends existing single-factor duration calculations to a multi-factor framework.

This issue aims to formally prove the covered and uncovered interest parity conditions within a Lean mathematical library. It involves deriving the no-arbitrage forward exchange rate formulas and ensuring consistency between covered and uncovered parity, referencing existing Black-Scholes model implementations.

This issue proposes formalizing the value of a concentrated-liquidity position in Uniswap v3 within a Lean formal verification framework. It requires deriving the token amounts and position value based on liquidity, price bounds, and the current price, and verifying boundary behaviors. The goal is to extend existing DeFi models with this new concept.

This issue involves formalizing the impermanent loss formula for a constant-product Automated Market Maker (AMM) in Lean. The task requires deriving the formula IL(r) = (2√r)/(1 + r) - 1 and proving that impermanent loss is always non-positive, with zero loss occurring only when the price ratio remains unchanged.

This issue proposes formalizing the Schwartz one-factor commodity futures closed-form solution. It involves applying the Ornstein-Uhlenbeck (OU) process to the logarithm of the spot price, similar to how it's used in the Vasicek bond pricing model. The goal is to derive the futures price formula using the Gaussian law of the OU state and ensure it satisfies the terminal boundary condition.

This issue addresses the lack of concrete implementations and tests for several theoretical concepts related to on-curve winding numbers in the Analysis/Contour module. The goal is to make these definitions load-bearing by proving key propositions, adding witness lemmas for regularity conditions, and ensuring existing computations are utilized.

This issue aims to improve and expand the existing API maps within the physics documentation. API maps are Markdown files that explain physics concepts and link to corresponding Lean code, with guidelines provided for their creation. This task is particularly suitable for newcomers to the project, especially those with a physics background, as the 'Alpha' phase maps are more amenable to changes.

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.

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.

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 `ZModCharges` in `ZMod.lean` incorrectly initializes the set `S`. The current initialization creates a set with a single element instead of the intended set of all possible charge spectra. The suggested correction uses `Finset.univ.filter` to correctly generate the desired set.

This issue requires enabling the `multiGoal` linter in the PhysLean project by adding a specific option to `lakefile.toml` and then addressing all generated warnings. The warnings are primarily stylistic, such as consolidating multiple `exact` tactics into a single line with bullet points.

This issue requires formalizing that the closed-form solution for the CIR model's bond loading B(T) satisfies its associated Riccati ordinary differential equation (ODE). The task involves proving B(T) is a `HasDerivAt` solution to B' = 1 - κB - ½σ²B² with the initial condition B(0) = 0, mirroring a pattern used for the Vasicek model.

This issue proposes adding SSZ (Simple Serialize) encoding for public keys and signatures within the xmss crate. The encoding involves a straightforward concatenation of byte vectors with specific lengths, and validation primarily focuses on ensuring the correct byte length.

This issue proposes a conjecture about the precise limiting ratio of the sequence $a_n$, which counts distinct flat foldings of a $1 imes n$ rectangular strip. While it's known that this limit exists and is within a specific interval, its exact value and whether it has a closed form or can be expressed using known constants remain unknown.

This issue aims to formalize the Feynman-Kac theorem for variable-coefficient diffusions, specifically starting with local volatility (σ(S,t)) and later extending to Heston models. This involves proving that the discounted expectation of a stochastic process solves a corresponding parabolic partial differential equation. The work is currently blocked by the availability of a general Itô/SDE layer.

The "Known gaps" section in the `docs/wifi-driver.md` file is outdated. It incorrectly lists calibrations and network functionalities (ARP/ping) as missing, when these have been implemented in recent commits. The issue requests an update to reflect the current state of the driver and to verify remaining gaps.

This issue proposes formalizing the Erdős-Faber-Lovász Conjecture, which states that if a graph G is an edge-disjoint union of n copies of the complete graph K_n, then its chromatic number is n. The primary challenge lies in formalizing the definitions of chromatic number and edge-disjoint graph unions within a formal proof system, as these are currently missing.

This issue identifies minor inconsistencies in the Heaplang logic related to memory allocation and heap adequacy checks. Specifically, `wp_alloc` is expected to return a `meta_token`, and the `heap_adequacy` function is missing an `inv_heap_inv` check. These are likely small code adjustments needed for correctness.

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 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.

This issue requests the formalization of the Balancer AMM invariant and its spot price formula within a Lean proof assistant. The task involves defining the generalized constant-mean invariant and deriving the spot price, then demonstrating its reduction to the simpler constant-product AMM case.

This issue requires proving a mathematical assertion about the size of a 'target-sum code' as stated in a specification. The proof involves demonstrating that a dynamic programming approach aligns with an inclusion-exclusion sum and then evaluating this sum, which is presented as a self-contained combinatorial problem.

This issue proposes adding a "tweak encoding" and a "tweakable hash" function to the XMSS cryptographic scheme. The tweak is a 16-byte value that identifies the specific use case of a hash operation within XMSS, ensuring distinctness between different calls and parameters.

This issue proposes adding a Continuous Integration (CI) job to the project that builds the library and its proofs. This new CI job would run on pull requests to catch broken proofs before they are merged, improving code quality and stability by complementing the existing CI which only runs on version tags.

This issue requires formalizing the present value of a whole-life insurance policy (A_x) in a mathematical formalization system. It also involves proving a fundamental identity that links A_x to the present value of a life annuity (ä_x) and the discount rate (d). The proof is described as a finite, algebraic manipulation of survival-weighted sums.

This issue presents Green's Open Problem #65, which asks whether a sufficiently large subset of integers, with a density of at least N^(1-c) for some c > 0, must contain a difference of two elements that is a non-zero square or a prime minus one. The problem is posed as a challenge for the community to add to the repository.