
Security News
Insecure Agents Podcast: Certified Patches, Supply Chain Security, and AI Agents
Socket CEO Feross Aboukhadijeh joins Insecure Agents to discuss CVE remediation and why supply chain attacks require a different security approach.
giftpy
Advanced tools
Formally verified mathematical relations from the GIFT framework. All theorems proven in Lean 4 and Coq.
The GIFT Certificate proves 180+ mathematical identities organized in five foundational pillars:
dim(E₈) = 248 = 240 roots + 8 rank
= 8 × 31 (Mersenne structure)
= 120 + 128 (SO(16) decomposition)
dim(G₂) = 14 = 12 roots + 2 rank
= GL(7) orbit stabilizer: 49 - 35
M₁ = Quintic in CP⁴: b₂ = 11, b₃ = 40
M₂ = CI(2,2,2) in CP⁶: b₂ = 10, b₃ = 37
─────────────────────────────────────────
K₇ = M₁ #_TCS M₂: b₂ = 21, b₃ = 77 (BOTH DERIVED!)
H* = b₂ + b₃ + 1 = 99
K₇ admits torsion-free G₂ structure
‖T‖ < 0.00141 vs threshold 0.0288 (20× margin)
Weyl Triple Identity: 3 independent paths to Weyl = 5
(dim_G₂ + 1) / N_gen = 5
b₂ / N_gen - p₂ = 5
dim_G₂ - rank_E₈ - 1 = 5
PSL(2,7) = 168: Fano plane symmetry
(b₃ + dim_G₂) + b₃ = 168
rank_E₈ × b₂ = 168
N_gen × (b₃ - b₂) = 168
The Certificate derives Standard Model parameters from topology:
| Relation | Formula | Value |
|---|---|---|
| Weinberg angle | sin²θ_W = 3(b₃+dim_G₂)/(13×b₂) | 3/13 |
| Koide parameter | Q = 2×dim_G₂/(3×b₂) | 2/3 |
| Generation count | N_gen | 3 |
| κ_T denominator | b₃ - dim_G₂ - p₂ | 61 |
| γ_GIFT | (2×rank_E₈ + 5×H*)/(10×dim_G₂ + 3×dim_E₈) | 511/884 |
| Ω_DE | (b₂ + b₃)/H* | 98/99 |
| m_τ/m_e | (b₃ - b₂) × 62 + 5 | 3477 |
See Lean/GIFT/Certificate.lean for complete theorem statements.
pip install giftpy
from gift_core import *
# Certified constants
print(SIN2_THETA_W) # Fraction(3, 13)
print(KAPPA_T) # Fraction(1, 61)
print(GAMMA_GIFT) # Fraction(511, 884)
# Lean 4
cd Lean && lake build
# Coq
cd COQ && make
Blueprint structure inspired by KakeyaFiniteFields.
MIT
GIFT Core v3.2.0
FAQs
GIFT mathematical core - Formally verified constants (Lean 4 + Coq)
We found that giftpy demonstrated a healthy version release cadence and project activity because the last version was released less than a year ago. It has 1 open source maintainer collaborating on the project.
Did you know?

Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.

Security News
Socket CEO Feross Aboukhadijeh joins Insecure Agents to discuss CVE remediation and why supply chain attacks require a different security approach.

Security News
Tailwind Labs laid off 75% of its engineering team after revenue dropped 80%, as LLMs redirect traffic away from documentation where developers discover paid products.

Security News
The planned feature introduces a review step before releases go live, following the Shai-Hulud attacks and a rocky migration off classic tokens that disrupted maintainer workflows.