Frederick Pu

UnluckyOrangutan

·

AI & ML interests

Automated theorem proving Reinforcement learning Computer Vision

Recent Activity

updated a model 24 days ago

UnluckyOrangutan/thomas-zhu-lean-premise-gguf

published a model 24 days ago

UnluckyOrangutan/thomas-zhu-lean-premise-gguf

updated a model 27 days ago

UnluckyOrangutan/joint-qwen-regression-gguf

View all activity

Organizations

None yet

UnluckyOrangutan 's datasets 15

UnluckyOrangutan/consts-mathlib-v4.30.0

Viewer • Updated Jun 13 • 368k • 21

UnluckyOrangutan/tactic-haveDraft11

Viewer • Updated Oct 18, 2025 • 443k • 11

UnluckyOrangutan/tactic-haveDraft10

Viewer • Updated Sep 8, 2025 • 429k • 17

UnluckyOrangutan/tactic-haveDraft9

Viewer • Updated Sep 5, 2025 • 104k • 9

UnluckyOrangutan/tactic-haveDraft8

Viewer • Updated Aug 23, 2025 • 449k • 17

UnluckyOrangutan/tactic-haveDraft7

Viewer • Updated Aug 11, 2025 • 307k • 13

UnluckyOrangutan/tactic-haveDraft6

Viewer • Updated Aug 10, 2025 • 307k • 9

UnluckyOrangutan/tactic-haveDraft5

Viewer • Updated Aug 9, 2025 • 323k • 8

UnluckyOrangutan/tactic-haveDraft4

Viewer • Updated Aug 7, 2025 • 302k • 15

UnluckyOrangutan/tactic-haveDraft3

Viewer • Updated Aug 5, 2025 • 484k • 56

UnluckyOrangutan/tactic-haveDraft2

Viewer • Updated Aug 4, 2025 • 514k • 23

UnluckyOrangutan/tactic-haveDraft

Viewer • Updated Jul 19, 2025 • 386k • 13

UnluckyOrangutan/tactic-have-pairs

Viewer • Updated Jul 16, 2025 • 21.6k • 14

UnluckyOrangutan/mathlib-traced-tactics

Viewer • Updated Jul 6, 2025 • 267k • 25

UnluckyOrangutan/leanworkbook-tactics

Viewer • Updated Jun 28, 2025 • 24