HN

Comments (12)

• austinvhuang
  Some may also find Junji Hashimoto's GPU programming library in lean (w/ webgpu) interesting:https://github.com/Verilean/hesperEven includes an example of transformer inference (quantized 1.5 bit):https://github.com/Verilean/hesper/blob/a688ce9848d6416b2e95...
• Menu

  westurner
  How could this lend insight into why Fast Fourier Transform approximates self-attention?> Because self-attention can be replaced with FFT for a loss in accuracy and a reduction in kWh [1], I suspect that the Quantum Fourier Transform can also be substituted for attention in LLMs.[1] "Fnet: Mixing tokens with fourier transforms" (2021) https://arxiv.org/abs/2105.03824 .. "Google Replaces BERT Self-Attention with Fourier Transform: 92% Accuracy, 7 Times Faster on GPUs" https://syncedreview.com/2021/05/14/deepmind-podracer-tpu-ba..."Why formalize mathematics – more than catching errors" (2025) https://news.ycombinator.com/item?id=45695541Can the QFT Quantum Fourier Transform (and IQFT Inverse Quantum Fourier Transform) also be substituted for self-attention in LLMs, and do Lean formalisms provide any insight into how or why?
• Menu

  measurablefunc
  I guess the next step would be adding support for quantized arithmetic.