Digesting Lean Data
Charles Norton
phanerozoic
AI & ML interests
Machina vincit omnia
Recent Activity
updated
a model
about 1 hour ago
phanerozoic/tiny-parity-prover
published
a model
about 3 hours ago
phanerozoic/tiny-parity-prover
liked
a dataset
about 22 hours ago
nvidia/Nemotron-Math-Proofs-v1
Organizations
models
33
phanerozoic/tiny-parity-prover
Updated
phanerozoic/BART-Large-CNN-Enhanced
0.4B
•
Updated
•
6
phanerozoic/BART-Large-CNN-Scratch
0.4B
•
Updated
•
5
phanerozoic/BERT-NER-Classifier
Token Classification
•
0.1B
•
Updated
•
192
phanerozoic/BERT-Sentiment-Classifier
Text Classification
•
0.1B
•
Updated
•
14
•
1
phanerozoic/BERT-Question-Classifier
Text Classification
•
0.1B
•
Updated
•
7
phanerozoic/Tiny-Pirate-1.1b-v0.2
Text Generation
•
1B
•
Updated
•
4
phanerozoic/Llama3-Pirate-Talk-8b-v0.1
Text Generation
•
8B
•
Updated
•
1
phanerozoic/Tiny-Viking-1.1b-v0.1
Text Generation
•
1B
•
Updated
•
3
phanerozoic/Tiny-Cowboy-1.1b-v0.1
Text Generation
•
1B
•
Updated
•
70
datasets
80
phanerozoic/Isabelle-Stdlib
Updated
•
14
phanerozoic/Isabelle-seL4
Updated
•
19
phanerozoic/Agda-Prelude
Updated
•
15
phanerozoic/Agda-HoTT
Updated
•
13
phanerozoic/Agda-Categories
Updated
•
27
phanerozoic/Agda-UniMath
Updated
•
25
phanerozoic/Agda-1Lab
Updated
•
14
phanerozoic/Agda-Cubical
Updated
•
26
phanerozoic/Lean4-Paperproof
Updated
•
16
phanerozoic/Lean4-Quote4
Updated
•
14