Frederick Pu's picture

1 1

Frederick Pu

UnluckyOrangutan

·

AI & ML interests

Automated theorem proving Reinforcement learning Computer Vision

Recent Activity

updated a dataset 1 day ago

UnluckyOrangutan/tactic-have-pairs

published a dataset 1 day ago

UnluckyOrangutan/tactic-have-pairs

upvoted an article 7 days ago

Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models

View all activity

Organizations

Articles 1

Article

39

Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models

models 1

UnluckyOrangutan/byt5-lean-goals

0.3B • Updated 16 days ago • 2

datasets 3

UnluckyOrangutan/tactic-have-pairs

Viewer • Updated 1 day ago • 21.6k

UnluckyOrangutan/mathlib-traced-tactics

Viewer • Updated 10 days ago • 267k • 88

UnluckyOrangutan/leanworkbook-tactics

Viewer • Updated 18 days ago • 127