Hacker News new | ask | show | jobs
by tough 518 days ago
The speaker is presenting a new AI tool that can synthesize proofs of mathematical theorems. The tool uses a combination of numerators and primitives to prove theorems exponentially fast, even on a single core. The speaker notes that the tool has limitations, such as only recursing on row numbers and not being able to learn or predict the next token in a symbolic transform. However, they believe that the tool will be useful for programming and solving big problems, such as the Riemann Hypothesis or making a whole game from scratch. The speaker plans to release a playground soon, allowing users to experiment with the tool and have fun using it.

Some key points from the presentation include:

* The tool can prove mathematical theorems exponentially fast, even on a single core. * It uses a combination of numerators and primitives to prove theorems. * It has limitations, such as only recursing on row numbers and not being able to learn or predict the next token in a symbolic transform. * The tool will be useful for programming and solving big problems. * A playground will be released soon, allowing users to experiment with the tool and have fun using it.

Overall, the speaker is excited about the potential of the tool and believes it could be a valuable addition to the field of AI research and development.
1 comments
tough 518 days ago
Table of Contents

01:53 Proving the Ruma Hypothesis - https://youtu.be/GddkKIhDE2c?t=113

  05:13 Restricting Word Types to Exactly Two Bits Set - https://youtu.be/GddkKIhDE2c?t=313

  05:18 First-Class Enumerations for Computation - https://youtu.be/GddkKIhDE2c?t=318

  06:35 Enumerations Interoperability - https://youtu.be/GddkKIhDE2c?t=395

  06:44 Narrowed List of Functions with Restrictions - https://youtu.be/GddkKIhDE2c?t=404

  07:50 New Definition Emerges - https://youtu.be/GddkKIhDE2c?t=470

  08:18 Section Title: Wrong Function Example - https://youtu.be/GddkKIhDE2c?t=498

  08:24 Most Overfit Functions, But First One Stands Out - https://youtu.be/GddkKIhDE2c?t=504

  09:40 General Addition Implementation Tested - https://youtu.be/GddkKIhDE2c?t=580

  09:49 Finding Unique Functions - https://youtu.be/GddkKIhDE2c?t=589

  10:36 Examining Functions with a Simple Loop - https://youtu.be/GddkKIhDE2c?t=636

  10:38 First Argument Relationship - https://youtu.be/GddkKIhDE2c?t=638

  10:48 PubShadow Literature Finds Problem in 0.06 Sec - https://youtu.be/GddkKIhDE2c?t=648

  11:37 Complexity Hides in Simple Tasks - https://youtu.be/GddkKIhDE2c?t=697

  12:11 Fast Loading Due to Under-the-Hood Optimizations - https://youtu.be/GddkKIhDE2c?t=731

  13:33 Function Finder in 4.5 Sec - https://youtu.be/GddkKIhDE2c?t=813

  13:41 Accelerating the Process - https://youtu.be/GddkKIhDE2c?t=821

  14:37 Speedups via Cluster Parallelization - https://youtu.be/GddkKIhDE2c?t=877
14:45 Boolean, Natural Number, Words of Fixed Length, Lists, Funct - https://youtu.be/GddkKIhDE2c?t=885

  16:23 Proving a Theorem by Defining an Empty Body - https://youtu.be/GddkKIhDE2c?t=983

  16:30 Recipient Receives First Bit of List - https://youtu.be/GddkKIhDE2c?t=990

  17:06 New Goal: Proving Equation for Pairs - https://youtu.be/GddkKIhDE2c?t=1026

  17:40 Section Title: Boolean List Conversion - https://youtu.be/GddkKIhDE2c?t=1060

  18:23 Constructing Equates in a Function - https://youtu.be/GddkKIhDE2c?t=1103

  19:07 True Case Match: Convert Not True to True - https://youtu.be/GddkKIhDE2c?t=1147

  19:21 Proof Complete: No More Obligations - https://youtu.be/GddkKIhDE2c?t=1161

  19:31 Proving Self-Computation with Auxiliary Function - https://youtu.be/GddkKIhDE2c?t=1171

  19:59 Proving List's Tail - https://youtu.be/GddkKIhDE2c?t=1199

  20:39 Inductive Hypothesis Applied to Rest of List - https://youtu.be/GddkKIhDE2c?t=1239

  21:29 Proof of Empty Pattern Match - https://youtu.be/GddkKIhDE2c?t=1289

  21:32 Section Title: Synthesizer's Turn - https://youtu.be/GddkKIhDE2c?t=1292
22:01 Demonstrating a Key Theorem - https://youtu.be/GddkKIhDE2c?t=1321

  23:05 Instant Search Proof - https://youtu.be/GddkKIhDE2c?t=1385
24:01 Enumerating the Proof Space - https://youtu.be/GddkKIhDE2c?t=1441

26:06 Integrating with Theorem Provers - https://youtu.be/GddkKIhDE2c?t=1566

27:20 Closing Notes: Simplistic Tool for Fast Solutions - https://youtu.be/GddkKIhDE2c?t=1640

28:08 Ready to Paralize with Cluster of Matchminis - https://youtu.be/GddkKIhDE2c?t=1688

  28:18 Predicting Next Token - https://youtu.be/GddkKIhDE2c?t=1698
29:18 Predicting Next Tokens with Symbolic Transforms - https://youtu.be/GddkKIhDE2c?t=1758

  29:33 Synthesizing Token Predictions from Lists - https://youtu.be/GddkKIhDE2c?t=1773
link