theorem
proved
phi_equation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.PhiForcing on GitHub at line 43.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
40noncomputable def φ : ℝ := (1 + Real.sqrt 5) / 2
41
42/-- φ satisfies the golden ratio equation: φ² = φ + 1. -/
43theorem phi_equation : φ^2 = φ + 1 := by
44 simp only [φ, sq]
45 have h5 : (0 : ℝ) ≤ 5 := by norm_num
46 have hsq5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
47 field_simp
48 nlinarith [Real.sq_sqrt h5, sq_nonneg (Real.sqrt 5)]
49
50/-- φ is positive. -/
51theorem phi_pos : 0 < φ := by
52 simp only [φ]
53 have h5 : Real.sqrt 5 > 2 := by
54 have h4 : (4 : ℝ) < 5 := by norm_num
55 have hsqrt4 : Real.sqrt 4 = 2 := by
56 rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
57 calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
58 _ = 2 := hsqrt4
59 linarith
60
61/-- φ > 1. -/
62theorem phi_gt_one : φ > 1 := by
63 simp only [φ]
64 have h5 : Real.sqrt 5 > 2 := by
65 have h4 : (4 : ℝ) < 5 := by norm_num
66 have hsqrt4 : Real.sqrt 4 = 2 := by
67 rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
68 calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
69 _ = 2 := hsqrt4
70 linarith
71
72/-- φ < 2. -/
73theorem phi_lt_two : φ < 2 := by
papers checked against this theorem (showing 30 of 31)
-
Trillion-parameter models scale recommendation quality with compute
"HSTU-based Generative Recommenders, with 1.5 trillion parameters, improve metrics in online A/B tests by 12.4% and have been deployed on multiple surfaces of a large internet platform with billions of users. More importantly, the model quality of Generative Recommenders empirically scales as a power-law of training compute across three orders of magnitude, up to GPT-3/LLaMa-2 scale."
-
3D model lets robots imagine futures before acting
"we train a series of embodied diffusion models and align them into the LLM for predicting the goal images and point clouds"
-
ALBERT sets new SOTA on GLUE, RACE and SQuAD with fewer parameters than BERT-large
"we also use a self-supervised loss that focuses on modeling inter-sentence coherence"
-
Position Interpolation extends LLM context to 32k tokens
"Our theoretical study shows that the upper bound of interpolation is at least ∼600× smaller than that of extrapolation"
-
Quantum algorithm solves Abelian stabilizer problem in polynomial time
"Another application of this procedure is a polynomial quantum Fourier transform algorithm for an arbitrary finite Abelian group."
-
New model unifies world simulation for robot training
"These capabilities enable more reliable synthetic data generation, policy evaluation, and closed-loop simulation for robotics and autonomous systems"
-
GPT-4 chain-of-thought scores text summaries closer to humans
"G-EVAL is a prompt-based evaluator with three main components: 1) a prompt that contains the definition of the evaluation task and the desired evaluation criteria, 2) a chain-of-thoughts (CoT) ..."
-
COCO supplies 1.5 million captions for 330k images
"Instructions for using the evaluation server are provided."
-
MMBench delivers bilingual test for all-around VLMs
"MMBench is a systematically designed objective benchmark for a robust and holistic evaluation of vision-language models"
-
LIGO-Virgo catalog ten compact binary mergers from first two runs
"For all significant gravitational-wave events, we provide estimates of the source properties... using relativistic models of GWs from CBCs"
-
Open dataset of 400 million CLIP-filtered image-text pairs released
"We use CLIP to compute embeddings of the image and alt-text. Then we compute the cosine similarity of both embeddings and drop all samples with cosine similarity below 0.3"
-
Text contexts compressed optically into vision tokens at 10x with 97% accuracy
"DeepSeek-OCR consists of two components: DeepEncoder and DeepSeek3B-MoE-A570M as the decoder."
-
Smart choices cut AI training carbon by up to 1000 times
"Large but sparsely activated DNNs can consume <1/10th the energy of large, dense DNNs without sacrificing accuracy despite using as many or even more parameters"
-
Fine-tuned LLaMA beats GPT-4 at writing API calls
"Gorilla's retriever–aware training enables it to react to changes in the APIs."
-
GRPO adaptation stabilizes RL for visual generators
"outperforms baseline methods by up to 181% across... HPS-v2.1, CLIP Score, VideoAlign, and GenEval"
-
RetNet matches Transformer scaling with O(1) inference
"RetNet achieves favorable scaling results, parallel training, low-cost deployment, and efficient inference"
-
DeepSeek-VL models match top VL benchmarks while keeping real-world usability
"The DeepSeek-VL family (both 1.3B and 7B models) showcases superior user experiences as a vision-language chatbot in real-world applications, achieving state-of-the-art or competitive performance across a wide range of visual-language benchmarks at the same model size while maintaining robust performance on language-centric benchmarks."
-
GLM-4.5 Hits 91% on AIME and 64% on SWE-Bench
"We present GLM-4.5, an open-source Mixture-of-Experts (MoE) large language model with 355B total parameters and 32B activated parameters, featuring a hybrid reasoning method that supports both thinking and direct response modes."
-
Janus-Pro boosts multimodal tasks and image generation via scaling
"decoupling visual encoding for multimodal understanding and generation"
-
67B DeepSeek LLM beats LLaMA-2 70B on code and math benchmarks
"Guided by the scaling laws, we introduce DeepSeek LLM, a project dedicated to advancing open-source language models with a long-term perspective."
-
Planck data favor concave potentials in slow-roll inflation
"Planck temperature, polarization, and lensing data determine the spectral index of scalar perturbations to be ns=0.9649±0.0042 at 68% CL and show no evidence for a scale dependence of ns."
-
RAG models top open QA benchmarks with Wikipedia retrieval
"We fine-tune and evaluate our models on a wide range of knowledge-intensive NLP tasks and set the state-of-the-art on three open domain QA tasks, outperforming parametric seq2seq models and task-specific retrieve-and-extract architectures."
-
3.8B model matches GPT-3.5 and Mixtral on a phone
"phi-3-mini achieves 69% on MMLU and 8.38 on MT-bench, rivaling Mixtral 8x7B and GPT-3.5"
-
Fresh contest problems expose LLM code benchmark overfitting
"we have evaluated 18 base LLMs and 34 instruction-tuned LLMs on LiveCodeBench"
-
RLHF aligns assistants as helpful and harmless while raising NLP scores
"identify a roughly linear relation between the RL reward and the square root of the KL divergence"
-
Open model reaches gold on 2025 IMO and IOI
"our high-compute variant, DeepSeek-V3.2-Speciale, surpasses GPT-5 and exhibits reasoning proficiency on par with Gemini-3.0-Pro, achieving gold-medal performance in both the 2025 International Mathematical Olympiad (IMO) and the International Olympiad in Informatics (IOI)"
-
Biggest models still far from expert on 57-task knowledge test
"We propose a new test to measure a text model's multitask accuracy. The test covers 57 tasks including elementary mathematics, US history, computer science, law, and more."
-
137-billion-parameter layer beats prior best LM at 6% the compute
"achieving greater than 1000x improvements in model capacity ... a MoE with up to 137 billion parameters is applied convolutionally between stacked LSTM layers."
-
Fine-tuning a 175B model needs only a rank-2 update
"We hypothesize that the change in weights during model adaptation also has a low 'intrinsic rank'... W0 + ΔW = W0 + BA, where B∈ℝ^{d×r}, A∈ℝ^{r×k}, and the rank r ≪ min(d,k)."
-
Drop the recurrence: attention alone tops translation benchmarks
"PE(pos,2i) = sin(pos/10000^{2i/d_model}); PE(pos,2i+1) = cos(pos/10000^{2i/d_model})"