{"id":"W14022547","doi":"","title":"Mechanising Hilbert's Foundations of Geometry in Isabelle","year":2008,"lang":"en","type":"article","venue":"Applied therapeutics","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":14,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"","keywords":"Mathematical proof; Axiom; HOL; Computer science; Calculus (dental); Forcing (mathematics); Programming language; Algebra over a field; Mathematics; Pure mathematics; Geometry","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":true,"about_ca":false,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0001971691,0.00009932516,0.0001652494,0.0001277977,0.0001068955,0.00002778134,0.0004313972,0.00007115416,0.000009052066],"category_scores_gemma":[0.000003335607,0.00009084377,0.0000394462,0.0005762661,0.00005572334,0.00009527151,0.00009396726,0.00009665499,0.0000415978],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003079214,"about_ca_system_score_gemma":0.00005100031,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004835352,"about_ca_topic_score_gemma":0.00001653351,"domain_scores_codex":[0.9991177,0.00002435074,0.0002438244,0.0002055778,0.0001953588,0.0002131524],"domain_scores_gemma":[0.9993641,0.00007855728,0.00009998264,0.000389659,0.00003692298,0.00003071227],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.000002771747,0.0001060305,0.000686949,0.00001027933,0.00002225308,0.000003071184,0.001861549,0.00003215909,0.004668863,0.9677858,0.00001786789,0.02480237],"study_design_scores_gemma":[0.002913109,0.0003258291,0.004208639,0.00001482135,0.00004287,0.0001102758,0.0007715482,0.01653506,0.09628625,0.7607396,0.1169272,0.001124835],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03274577,0.0002922285,0.9462433,0.0001821322,0.0003023214,0.0002892955,3.465574e-7,0.0001131959,0.01983136],"genre_scores_gemma":[0.9911484,0.00004208603,0.008359768,0.0002170733,0.00003179258,0.00001333653,0.000002016475,0.000009247403,0.0001762656],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9584026,"threshold_uncertainty_score":0.3704501,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04865476613072473,"score_gpt":0.2663759915727779,"score_spread":0.2177212254420532,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}