{"id":"W4415087038","doi":"10.1109/synasc69064.2025.00022","title":"Structuring Definitions in Mathematical Libraries","year":2025,"lang":"en","type":"article","venue":"","topic":"Mathematics, Computing, and Information Processing","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Structuring; Process (computing); Usability; Automated theorem proving; Algebra over a field; Symbolic computation; Documentation; Gas meter prover","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0001482191,0.00006937007,0.0001068959,0.0002044538,0.0001012806,0.0003644726,0.0004156765,0.00003126763,0.00008096263],"category_scores_gemma":[0.0001038388,0.00005964755,0.00002431258,0.000384458,0.00002642217,0.0009886356,0.0002321097,0.00008029294,0.00004774826],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00001472232,"about_ca_system_score_gemma":0.00007643803,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000001418862,"about_ca_topic_score_gemma":0.000001004962,"domain_scores_codex":[0.9993131,0.00001179778,0.0003195528,0.0001092636,0.00009942922,0.00014683],"domain_scores_gemma":[0.9995428,0.0001303953,0.00004694538,0.000227749,0.00002713203,0.00002492776],"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":[1.612613e-7,0.00001281069,0.00007331531,0.00008774106,0.000001862725,5.140109e-7,0.001027613,0.00006398052,0.000003163744,0.9933547,0.0003128401,0.00506125],"study_design_scores_gemma":[0.00008855037,0.000002202742,0.0002413909,0.00007678445,7.366477e-7,0.000003415812,0.0001118716,0.2673962,0.0007017569,0.7310171,0.0003036189,0.00005640958],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.003506312,0.00001847677,0.7077538,0.0004351078,0.00006522865,0.0000419176,1.122314e-7,0.0001448772,0.2880341],"genre_scores_gemma":[0.5185938,0.00000314731,0.479979,0.0007433158,0.000009087147,0.000006077926,6.391619e-7,0.000002309414,0.0006625711],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.5150875,"threshold_uncertainty_score":0.3514618,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02665461323106826,"score_gpt":0.2458338802550512,"score_spread":0.2191792670239829,"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."}}