{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.03846803,0.001185199,0.001408582,0.01106322,0.006768895,0.01993214,0.004102473,0.003127054,0.009425683],"category_scores_gemma":[0.06752101,0.001959361,0.002526189,0.01104897,0.01750722,0.04604401,0.01373827,0.006858453,0.004144195],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.006381786,"about_ca_system_score_gemma":0.005924649,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001753749,"about_ca_topic_score_gemma":0.002463944,"domain_scores_codex":[0.9547557,0.02595311,0.005913948,0.004293711,0.007208427,0.001875106],"domain_scores_gemma":[0.9301568,0.04264028,0.004398361,0.01415821,0.007560331,0.001085994],"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.00001521649,0.00001367543,0.0003571997,0.0003431479,0.00001166375,0.00006297288,0.004329396,0.0005116235,0.0003995795,0.955337,0.003842684,0.03477586],"study_design_scores_gemma":[0.00001649666,0.00003204848,0.0002987066,0.0006090908,0.00002727738,0.0003232733,0.001741687,0.001954579,0.002192475,0.6637993,0.3289504,0.00005468987],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01498319,0.00954941,0.9220802,0.006304288,0.0005864142,0.0003494851,0.0004156267,0.00276129,0.04297013],"genre_scores_gemma":[0.1323966,0.005732826,0.8395003,0.002901695,0.0006675641,0.0005847506,0.0009598504,0.002821526,0.01443483],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.03846803,"threshold_uncertainty_score":0.2034408,"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."}}