Article

Obsidian Source: 2025-05-07

Summary

Pending synthesis from local Obsidian source.

Original source title: 2025 05 07

Extracted Preview

Lean and LLMs. Please if we do this Deepmind will come to us.

AlphaEvolve and some other work is similar to this. Previous work include FunSearch:

_We introduce FunSearch, a method to search for new solutions in mathematics and computer science. FunSearch works by pairing a pre-trained LLM, whose goal is to provide creative solutions in the form of computer code, with an automated “evaluator”, which guards against hallucinations and incorrect ideas. By iterating back-and-forth between these two components, initial solutions “evolve” into new knowledge. The system searches for “functions” written in computer code; hence the name FunSearch._

!Pasted image 20250515122816.png

This is for AlphaEvolve

!Pasted image 20250515122916.png

_AlphaEvolve can also propose new approaches to complex mathematical problems. Provided with a minimal code skeleton for a computer program, AlphaEvolve designed many components of a novel [gradient-based optimization](https://www.sciencedirect.com/topics/engineering/gradient-based-algorithm) procedure that discovered multiple new algorithms for matrix multiplication, a fundamental problem in computer science._

_AlphaEvolve can be applied to any problem whose solution can be described as an algorithm, and automatically verified._

Resources:

Integration Notes

  • Source folder: /home/yashs/Documents/Docs/Obsidian/Research-Notes
  • Local source: /home/yashs/Documents/Docs/Obsidian/Research-Notes/2025-05-07.md
  • Raw copy: raw/obsidian/research-notes/2025-05-07.md

Links Created Or Updated

Open Questions